目についたCoqのライブラリ/プラグイン/開発環境などの覚え書き
実用面は気にせず、研究用や無メンテも載せる
Coqソースファイルのみで構成されるもの
機能拡張的なものと定理群の区別はしていない
-
-
数学的証明を書き易くするための諸々
-
-
-
ホモトピー型理論
-
-
-
IOを伴うプログラムが書ける (OCamlに抽出)
-
-
-
IOや例外等を定義し、OCamlに抽出出来るように紐付け
-
-
-
引数リストを使って関数をテストできる
-
-
-
引数生成関数を使って関数をテストできる
-
-
-
演繹的プログラム合成
-
仕様を詳細化(refine)していくことで関数(≒実装が一意に定まる仕様)を組み上げていく
-
Facadeを経由してBedrockへの変換・リンクも可能
-
-
-
篩型の制約を実行時検査するようなOCamlプログラムを抽出できる
-
-
-
関数の計算量を証明できる
-
似たような研究はいくつかある
-
-
-
等式変形などの証明パターンをより自然な記法で行える
-
-
-
Falseの証明(バグを用いたもの)
-
OCamlによってCoqに機能を追加しているもの
-
-
QuickCheckのCoq版
-
-
-
Template Coq(MetaCoqの一部)の改良版
-
Coqの内部表現をCoqで扱える値として引きずり出す
-
-
-
GCを強制実行
-
-
-
命令型プログラミングが扱える
-
-
-
証明を宣言的証明に変換する
-
-
-
定義済み関数をモナド化し、計算量などの証明を可能にする
-
-
-
引数に関するパターンマッチを使って関数定義ができる
-
-
-
一部の定理の型を変更した時に、それに依存する証明を楽に修正できる
-
-
-
Parametricityによる同値関係を生成できる
-
-
-
rewirteに都合の良いヒントDBを作る
-
-
-
Coqで入出力などの作用を持つプログラムを定義する
-
-
-
再帰や状態を持つ言語を定義するための便利ライブラリ
-
-
-
高速なタクティックを作れる
-
-
-
型付きタクティックを作れる
-
-
-
型システム載せたり文法を少し変えたりした便利なLtac
-
-
-
SMTで証明項を生成するタクティックを追加する
-
-
-
Coq版Sledgehammer
-
E、Z3、Vampireを使っている
-
-
-
反例生成器Nunchakuをゴールに対して適用するタクティックを追加する
-
-
-
既存の証明スクリプトを元に今使えそうなタクティックを提案する
-
提案タクティックを使って自動証明させることもできる
-
-
-
機械学習による証明生成ツール
-
Coqとは独立したPythonスクリプト
-
-
-
定理等の依存関係をグラフ化
-
JSON形式で出力するhttps://github.com/proofengineering/coq-dependsも
-
-
-
ASTをJSON形式で出力
-
-
-
現在のゴールがSMTで解けるか教えてくれる(証明項は生成しない)
-
-
-
miniMLのASTからPythonのASTに変換し、OCamlのPythonライブラリを使って出力している
-
都合の悪いコード(同じ名前の変数を複数回宣言など)があるとエラーを吐く仕様
-
-
Scala(v8.4)
-
Coqで書いてるらしいがExtractionしたOCamlしかない
-
miniMLに対して型推論することで型情報を補間している
-
論文もある
-
-
-
Coqで書いた変換コードをOCamlにExtractionしている
-
ここの解説がExtraction拡張の概要をつかむには便利かも
-
-
-
Haxe経由でC++とかJavaとかJavascriptとか諸々に変換可能なはず
-
-
-
抽出したSchemeをCommon Lisp等で使えるように変換する
-
-
-
より自然言語っぽく書ける証明ソフト
-
-
GeoProof(故)
-
Coqを利用した幾何証明ソフト
-
-
-
自然言語解析ツール
-
-
-
SMTやC等をCoqで証明できる
-
-
-
言語定義をCoqにしたりやLaTeXで表したり
-
-
-
言語の一部の性質をCoqで証明できる言語ワークベンチ
-
ツール全体からするとおまけ的な機能っぽい
-
-
-
Coqをバックエンドに持つプログラミング言語
-
-
-
プログラムを作って各種証明アシスタントに投げられる
-
-
-
OCamlをCoqに変換する
-
-
-
HaskellをCoqに変換する
-
-
Concoqtion (故)
-
OCamlに依存型を導入して、証明が必要な部分だけCoqを使う
-
-
-
Coqの命題とOCamlのプログラムを吐くCoqよりリッチ目な言語
-
-
-
Rustでunsafeを使っても大丈夫なことを証明する
-
-
-
GoのコードをCoqに変換して証明できるようにする
-
-
-
mliファイルから対応するCoq定義を生成し、依存関係を持つOCamlプログラムをいい感じに抽出出来るようにする
-
-
Fellowship (故)
-
CoqとPVS両方の証明記述を生成できるsuper-prover
-
-
-
Coherent Logicを使った証明アシスタントで、CoqとIsabelle両方の証明を吐ける
-
-
-
SQLクエリの等価性を自動証明し、Coq形式で出力する
-
-
-
coqdocの証明部分に各ステップの状態を表示する機能を追加する
-
-
-
証明を動的に表示/非表示できたり特定文字列を置換できたりするcoqdoc亜種
-
-
-
証明が折りたためるcoqdoc亜種
-
-
-
Coqコードから各行の実行結果を併せて表示するHTMLを生成する
-
表示形式を選べることが特徴で、単に記号を使うだけでなく図示等も可能
-
-
-
coqdoc形式のファイルをmarkdownに変換する
-
-
-
Coqの証明をXMLに変換してwebで見る (8.4あたりまで搭載されていた？)
-
-
-
Coqの証明内の基本タクティックに対し、その動作を示すコメントをつける
-
-
-
Coqの型定義を元に推論規則を表すLaTeXを生成する
-
-
-
Coqの証明をステップごとにゴールと自然言語で表現することで可読にする
-
-
-
証明の一部が変更された時、関係する証明のみチェックする
-
-
-
不要なImportコマンドを消す
-
-
-
Coqが吐くログを整理する
-
-
-
Coqの証明を機械学習で生成する
-
-
-
Coqを操作するAPIを提供する
-
-
-
Coqの利用データを記録する(統計データ収集を想定)
-
-
-
Coqプロジェクト用のGithub Action
-
-
-
CIC(だいたいGallina)の形式化
-
-
-
100定理形式化
-
-
-
倉庫番 (ゲーム)
-
-
-
Coqでアプリが書ける？
-
-
-
証明付きJavaScript
-
-
-
証明付きC
-
-
-
証明アシスタントNuprlのCoq版
-
-
-
Persec風パーサコンビネータ
-
「"1+1"はexprである」などの命題が書けるようになる
-
-
-
シリアライザ
-
自前の型については自分で両方向の変換と証明を書く必要がある
-
Coqでこれを使ってプログラムを書いた後、OCcamlに抽出して使うことを主に想定していると思う
-
-
-
自然言語(英語)の意味論をCoqで扱う試み
-
同テーマのチュートリアル資料も参考になるはず
-
主に抽出によって実行ファイルが生成されるようなもの
-
-
Coqで証明されたCコンパイラ
-
-
-
Coqウェブサーバ
-
Dockerfilleを見るとわかるように、多くのライブラリを使っている点に注意
-
-
-
ブログエンジン
-
-
-
Coq製LLVM
-
他にもDeepspecではOSやハードウェア記述言語をCoqで作る試みも
-
-
-
Coqによって幾つかの安全性が示されているブラウザ
-
Coq製カーネル部はOCamlに抽出し、ガワはPythonを使っている
-
-
-
Fitch記法に基づく小さな証明言語
-
Ottで言語定義している
-
-
-
ファイルシステム
-
Coq・OCaml・Haskell・Goのハイブリッド
-
-
-
クエリコンパイラ
-
ソース言語とターゲット言語をそれぞれ複数持つ
-
既存の証明を形式化した話なら探せば沢山ある
-
-
Coqによる証明の中でも代表的なやつ
-
元の証明では(膨大な場合分けに対応するため？)一部でプログラムを使っていたのでバグが心配だったが、Coqで形式化することで信頼性が増した
-
-
-
証明されてはいたが非常に難しかったので形式化した
-
6年かかった
-
-
-
既存のデータ構造の永続版を作り、その正当性を証明した
-
-
-
形式化しながら議論してるらしい
-
現在はAgdaやLeanでもやってる
-
-
-
CoqでCoqを形式化や検証する
-
-
Papuq (CoqIDE拡張):とりうる選択肢を英語で提示
-
rlwrap (coqtop拡張？):カーソル移動やコマンド履歴呼び出し、入力補完ができるようになる
-
HenBlocks (JsCoq拡張):Scratch風WebIDE