Coq/SSReflect/MathCompの設定
[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 (
OCamlとCoqでブロックチェーンプログラミング
2019年7月29日、Opt Technologiesが主催するイベント「Fun Fun Functional (2) 関数型言語Lightning Talks!!」が開催されました。関数型プログラミングについて楽しく学び、知見を共有することを目的に開催されている本勉強会。今回は6名のエンジニアが、関数型プログラミング言語にまつわるユニークな発表を行いました。プレゼンテーション「OCamlとCoqでブロックチェーンプログラミング 」に登壇したのは、yoshihiro503氏。 OCamlとCoqでブロックチェーンプログラミング yoshihiro503氏（以下、yoshihiro503）：みなさんこんにちは。こういう鶏のアイコンのyoshihiro503です。今日「OCamlは良いぞ！」という話をします。株式会社ドワンゴのDMC開発部に所属しています。 簡単に自己紹介を
CFML: Characteristic Formulae for ML
CFML is a tool for the interactive verification of OCaml programs, using Coq and Separation Logic. The source files can be obtained from: git clone git@github.com:charguer/cfml.git For installation instruction, read the README file.The developments rely on my Coq library TLC.All the files are distributed under the GNU-LGPL license.
CoqのtacticをOCamlで書く話 - 簡潔なQ
CoqのtacticをOCamlで書いてみたので、同じようなことをしたい人のためにメモ。 なお私はOCamlについてはそれほど詳しくないので、そこの正確性については注意が必要。 同じ事をしているtacticがないか探す 同じようなことを考えている人は必ずいるはず。といっても、網羅的な探し方があるわけではないので、ある程度調べて見つからなかったら自分で書いたほうが効率が良いかもしれない。 まずCoq自体にないかを調べる。Coqの基本的なtacticsは Tactics Indexに書かれている。 Coqのcontribution集に似たような内容のものがないかを調べる。contributionは の「All contribs」というリンクから一覧できる。 特に、AACTacticsは有用らしく、Ubuntuのパッケージにもなっているようだ。 ssreflectには有用なtactic/tact
OCamlとCoqを連携してIO処理をモナディックに扱う - にわとり小屋でのプログラミング
この記事は OCaml Advent Calendar の5日目の記事です。 OCamlと連携して、CoqでもIO処理ができるようにするためのライブラリを作った。 http://github.com/yoshihiro503/coqio このライブラリを使えば、例えば次のようなコードを書くことができる。 Require Import Monad IO. Open Scope string_scope. Definition main : IO unit := do _ <- print "Hello" ; println ", world!". Haskell風のdo式みたいな記法が便利だね。print関数には文字列だけでなく、Showクラスのインスタンスとなる型を持つ式ならばなんでも与えることができる*1。 このコードを次のコマンドでExtractすればcoq.mlというOCamlのソー
OCamlでlet recを使わずにfact関数を定義する - にわとり小屋でのプログラミング
今日はProofCafeでCPDTの三章を読み進めたが、そこでCoqではInductive型のコンストラクタの引数が関数のとき、その関数の左側に自分自身が現れてはいけないということを学んだ。もしそれを可能にしてしまうと無限ループが定義でき、公理系が矛盾してしまうからだ。次のシンプルな例を見てみよう。 Inductive t (A: Set) : Set := | T : (t A -> A) -> t A. 一見なんの問題も無さそうな この型定義は失敗し、次のようなコンパイルエラーが出力される。 Error: Non strictly positive occurrence of "t" in "(t A -> A) -> t A".もしこの型が定義できたとすると次のような関数が定義できてしまう。 Definition ワォ (T f) := f (T f). ここで (ワォ (T ワォ)
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
