Verlang と Coq の Extraction について - Qiita
この記事は Theorem Prover Advent Calendar 2014 の5日目の記事です。 昨日は notogawa さんの ブラウザ上でAgdaを試せるサイトを作ってみた でした。Try Agda、前に見せていただいたときよりかなり綺麗になっててビビりました。自分の ProveEverywhere はやるやる言いながら放置なので、ダメですね… さて、本題ですが、Coq には Extraction という、Coq のコードを別の言語に変換する機能があり、この機能によってコードを検証済みの部品として実際のプログラムに使えるようになっています。標準では OCaml, Haskell, Scheme への変換が可能になっています。 この記事では、Verlang という、Coq の Extraction 対象に Erlang のコア言語である Core Erlang を加えるパッチ
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://www.psg.cs.titech.ac.jp/files/ppl2016_actario_poster.pdf
GitHub - tcarstens/verlang
