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 を加えるパッチ
wercker を使って Coq コードを CI する - Qiita
wercker の Coq box をけっこう前に作っていたのでその紹介です。 wercker は Travis CI のような CI as a Service と呼ばれる類の Web サービスです。基本無料です。 wercker では任意のアプリケーションをインストールした環境 (box といいます) を自分で作ることができて、その環境を使って CI をすることができます。 使い方 GitHub または Bitbucket にリポジトリ (Private でも可) を作り、wercker にそのリポジトリを登録します。 Make というファイルを作り、下のように Coq ファイルの名前を書いていきます。 ファイル名は Make でなくてもいいのですが、Coq演習第7回 に「Makeという名前にすることが多い」と書いているとおり ssreflect やその他いろいろなライブラリで Make
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
