Verlang と Coq の Extraction について - Qiitaこの記事は Theorem Prover Advent Calendar 2014 の5日目の記事です。 昨日は notogawa さんの ブラウザ上でAgdaを試せるサイトを作ってみた でした。Try Agda、前に見せていただいたときよりかなり綺麗になっててビビりました。自分の ProveEverywhere はやるやる言いながら放置なので、ダメですね… Verlang と Coq の Extraction について さて、本題ですが、Coq には Extraction という、Coq のコードを別の言語に変換する機能があり、この機能によってコードを検証済みの部品として実際のプログラムに使えるようになっています。標準では OCaml, Haskell, Scheme への変換が可能になっています。 この記事では、Verlang という、Coq の Extraction 対象に Erla
