2009-12-01から1ヶ月間の記事一覧

refineタクティックでらくらく依存型プログラミング(?)

Coq

下の記事では, Definition dual_dec : forall (u1:sesstyp) (u2:sesstyp), {dual u1 u2}+{~dual u1 u2}. という関数を,Coqの証明モードで作りました.ところが証明モードで作ったプログラムは極めて複雑でイマイチ効率のほどがよくわかりません (Coqで Pri…

セッション型(一部)の双対の決定可能性を証明

Coq

すごくどうでもいい証明です..Coqを触るのは2年ぶりくらいだろうか… めちゃくちゃ非効率なことをやっていそうなので,皆さんのツッコミをお待ちしています. 前提 セッション型の双対とは,受信の双対が送信,送信の双対が受信という感じで決まっています…