CoqからのCプログラム生成 田中 哲 産業技術総合研究所 情報技術研究部門 2017-07-23 Proof Summit 2017
CoqからのCプログラム生成 田中 哲 産業技術総合研究所 情報技術研究部門 2017-07-23 Proof Summit 2017 2/48 元ネタ ● 既発表の話です ● そのうち論文が出ます ● Safe Low-level Code Generation in Coq using Monomorphization and Monadification Akira Tanaka, Reynald Affeldt, Jacques Garrigue IPSJ SIGPRO 114, 2017-06-09, will be appear at IPSJ JIP. ● ここで出てくる plugin は github にあります – https://github.com/akr/monomorphization – https://github.com/akr/monadification
プログラミングCoqの2章をHaskellに翻訳してみた - maoeのブログ
皆さん、小悪魔CoqチュートリアルことプログラミングCoq読んでいますか？僕は大変楽しく読ませていただいています。今日第2章にあたるProof-editing mode であそぼうが公開されました。今回はCoqの証明支援の側面がよくわかる章になっていて興味深いのですが、扱っている命題はまだ簡単で、Haskellでも十分表現できそうです。 というわけでHaskellに翻訳してみました。 今回、Haskellの拡張をいくつか使っています。 Coqの表記と対応関係を取るためにExplicitForAll（Rank2Typesで自動的に有効になる） prop1で、forall付きの型を引数に取る関数の型を表現するためにRank2Types orとandを表す型を演算子で表すためにTypeOperators こうしてみてみると、Coqが自動的に作った仮定がHaskellにおける仮引数に対応づけられて
■ - ひとり勉強会
ここ「ひとり勉強会」は、会と言いつつひとりで勉強した記録を残してます。 Coq の解説記事を書くために勉強しています。 (1): forall A B: Prop, (A->B) -> A -> B. CoqIDEのつかいかた。forall と -> の証明。 (2): forall A B: Prop, ~(A ∨ B) -> (~A ∧ ~B). and と or と not の証明。Inductive な命題。 (3): forall n: nat, exists m, (n=2*m ∨ n=2*m+1). 自然数やリスト。再帰的 Inductive なデータ。= と 帰納法 と exists の証明。omega, ring, field による自動証明。標準ライブラリの使い方。 (4): 解説テキストリンク集 (番外編): VSTTE 2012 Software Verificat
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
