yoshihiro503の日記

2010-03-31

[]Proof Cafe (栄) Proof Cafe (栄) - yoshihiro503の日記 を含むブックマーク はてなブックマーク - Proof Cafe (栄) - yoshihiro503の日記

証明されたプログラムを作ろう!

Coqでリストを定義し、そのうえでのappendやlengthなどの基本的な関数を実装します。そして簡単な性質を証明しましょう。それができたら証明されたプログラムの完成です!となりの人と組んでペアプルしましょう。Coqや形式手法に興味のある人は大歓迎です。MLHaskellなどの関数型言語の経験があると理解は早いでしょう。

[追記]

id:mzpがまとめを作ってくれました。 ProofCafe 第1回 - Togetterまとめ