Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (Texts in Theoretical Computer Science. An EATCS Series)Springer2004/0511Yves BertotPierre CastéranG. HuetC. Paulin-Mohring読んだ読みたいamazonで見る
ハッカーのたのしみ―本物のプログラマはいかにして問題を解くかエスアイビーアクセス2004/094ジュニア,ヘンリー・S. ウォーレンJr.,Henry S. Warren滝沢 徹玉井 浩鈴木 貢赤池 英夫葛 毅藤波 順久読んだ読みたいamazonで見る