id:keigoiさんが面白いことをやっていたので，定義をお借りして勝手に証明の続きを書いてみた．元記事はこちら→OCamlコードをCoqで検証できる "CFML" で 証明コンペに挑戦 (未完)． CFML を使った感想 CFML とはなんぞや，というのは元記事を参照して頂くと…

なんとなくはてなダイアリーを始めてみた．