There is a recent interest for the verification of monadic programs using proof assistants. This line of research raises the question of the integration of monad transformers, a standard technique to combine monads. In this paper, we extend Monae, a Coq library for monadic equational reasoning, with monad transformers and we explain the benefits of this extension. Our starting point is the existin
[2023-02-24 Fri]: Ubuntu 22.04.1 LTS, Coq 8.16.1, MathComp 1.16 [2023-01-06 Fri]: Ubuntu 22.04.1, opam 2.1.4, ocaml 4.14.1, Coq 8.16.1, ProofGeneral 4.6, MathComp 1.15.0, MathComp-Analysys 0.6.0 [2022-09-09 Fri]: Ubuntu 22.04.1, Coq 8.15, MathComp 1.15 (opam), ProofGeneral 4.6 [2022-08-03 Wed]: Windows 11, Coq 8.15, MathComp 1.15 (WSL 2) [2022-03-01 Tue]: Windows 11 21H2, Coq 8.15, MathComp 1.14 (
この記事は言語実装 Advent Calendar 2020 の5日目の記事です. 一度でも型推論器を書いたことがあれば,そのあまりの邪悪さ,あるいはその複雑さに恐れ慄いたことでしょう. 参照を用いて単一化を実現しようものなら構文木は参照に汚染され,純粋関数型に実装しようものなら大量の型代入をどのような順序で適用したものか悩まされる. これは Hindley-Milner 型推論器を実装する上での宿命のようなものです. 本記事では,MLのサブセット——型付きλ計算をletと参照で拡張した,let多相をサポートする言語——の型推論器を Coq で実装し,その正当性を証明します. Coq で検証を行うことで我々は型推論器のバグへの恐怖とデバッグの労力から真に解放され,枕を高くして眠ることができることでしょう. もっとも、型付きλ計算を let 多相で拡張した言語の型推論器の正当性は実はすでに証
2019年7月29日、Opt Technologiesが主催するイベント「Fun Fun Functional (2) 関数型言語Lightning Talks!!」が開催されました。関数型プログラミングについて楽しく学び、知見を共有することを目的に開催されている本勉強会。今回は6名のエンジニアが、関数型プログラミング言語にまつわるユニークな発表を行いました。プレゼンテーション「OCamlとCoqでブロックチェーンプログラミング 」に登壇したのは、yoshihiro503氏。 OCamlとCoqでブロックチェーンプログラミング yoshihiro503氏(以下、yoshihiro503):みなさんこんにちは。こういう鶏のアイコンのyoshihiro503です。今日「OCamlは良いぞ!」という話をします。株式会社ドワンゴのDMC開発部に所属しています。 簡単に自己紹介を
僕の所属する研究室では毎年Software Foundationsの輪講をやっているんですが,Brzozowski derivativeに基づいて正規表現エンジンを実装し,あまつさえCoqで検証してしまおうといった練習問題が追加されていて大変興味深かったです. 折角practicalなプログラムを書いたのにCoqの中に閉じ込めておくのも勿体ないですし, OCamlで同様の正規表現エンジンを実装し,実行速度を見てみようと思います. *1 2018/12/16 Brzozowski derivativeの定義に誤りがあったため修正 Brzozowski derivativeとは? ある正規表現が受理する言語の先頭から,文字を取り除いて得られる言語 *2を受理する正規表現をBrzozowski derivativeといい,以下のようにsystematicに求められます. ある正規表現が空文字列を
2016年9月に次の記事を書きました。 関数型プログラミングとオブジェクト指向について、何か書く、かも タイトルからして引き続く記事を予告しているのですが、その予告を実行することができませんでした。タイトル中の「何か」とは「型クラス」のことです。上記の記事の最後の部分は: 関数型プログラミングにもオブジェクト指向にも関係があって、今後重要度を増すであろう「型クラス」ですが、今述べた(愚痴った)ような事情で(あと、C++のコンセプトは宙ぶらりんだし)、説明の方針も題材も定まりません。でも、いつか、何か書く、かも。 今回この記事で、予備知識をあまり仮定しないで型クラスの説明をします。言いたいことの1/3くらいは書きました。1/3でも長い記事なので、ぼちぼちと読んでもらえれば、と。書き残したことは最後に触れます。いつか、1年はたたないうちに(苦笑)、続きを書くつもりです。 内容: Haskell
この記事は、Theorem Prover Advent Calender https://qiita.com/advent-calendar/2017/theorem-prover のために書かれました。 Coqをある程度知っている人向けの小ネタです。 しばしばCoqの紹介において、「Coqでは停止するプログラムしか書けない」「(そのため)Coqはチューリング完全ではない」と言われることがあります。実はこれ、正しいと言えば正しいのですが、間違いと言えば間違いです。 確かに、Coqで再帰関数を定義するためのFixpoint, Program Fixpoint, Functionといったコマンドはどれも停止性を要求します。そのため、Coqから抽出したプログラムは無限ループを起こすことはなく、その意味で安全性が保証されることになります。 では、何が間違いか? これは「Coqでは停止するプログラム
We present an architecture of a full hammer for dependent type theory together with its implementation for the Coq proof assistant. A key component of the hammer is a proposed translation from the Calculus of Inductive Constructions, with certain extensions introduced by Coq, to untyped first-order logic. The translation is "sufficiently" sound and complete to be of practical use for automated the
これは Theorem Prover Advent Calendar 2016 の5日目の記事です。 はじめに オフラインリアルタイムどう書くというプログラマ向けイベントがあります。オフラインで集まって、主催者が出したプログラミング課題を参加者が制限時間内に解いて、回答を発表しあうというものです。そこで過去に出題された課題に対してCoq/SSReflectを使った回答を試みた、というのがこの記事の趣旨です。さすがにイベントで回答するには時間が足りなさすぎるので、自宅で解きました。この記事で扱う問題はこれです。 五角形の世界であなたは過去の自分に出会う 五角形で敷き詰められた升目を移動するためのコマンド列が与えられるので、閉路を見つけなさいという問題です。詳細はリンク先をご覧ください。回答を試みたところ、結果的にこうなりました。 自分なりに回答した。問題を自分なりに定式化して、その仕様を満た
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く