http://www.infoq.com/jp/articles/coqtutorial記事は速攻で仕上げました。 毎度のことですが、@tmiya_さんに感謝です。 個人的に、Coqチュートリアル実施の意味は大きい。 実施するまでは、「チュートリアル自体に目新しいことはない」 という意識があった…

P18に掲載されているものをCoqで。 http://gist.github.com/963772 Pab Pba ----------------------------- split. forall x, exists y,Pxy Pab & Pba ---------------------- -------------------- exists y. exists y,Pay. exists y,(Pay & Pya). --------…

証明途中ですが。https://gist.github.com/954854

議題 名前空間を完全に分離したいときは、ファイルを分けるのが無難。 Coq内でのLoad Pathの設定方法 Add LoadPath "~/src/coq/ConCaT" as ConCaT. Print LoadPath. Require Export ConCaT.SETOID.Map2. structureをlocalにできるのか？ ConCaTのインストー…

http://gist.github.com/936114先週の続き。 ごく普通の関数型プログラミングの流れ、という気がする。

https://gist.github.com/936114証明＝プログラムという感覚が不思議、かつおもしろい。

http://www.cis.upenn.edu/~bcpierce/sf/少しずつ進めることにした。 http://gist.github.com/933961これは基本的に自習教材だなぁ。

http://atnd.org/events/15000というのが企画されています。 圏論の話がわからない私にとって、 ヒントになるかなー。

http://www.cse.chalmers.se/research/group/logic/book/book.pdfこれは後で読むことにする。 3連休はCategory Theoryの読書として、 "Category Theory",Steve Awodey "CATEGORIES AND COMPUTER SCIENCE", R.F.C.Walters "Conceptual Mathematics",F.William…

tmiyaさんが出している問題に触発されました。 http://study-func-prog.blogspot.com/2010/07/coq-coq-99-part-1.html数をこなせば自然と出来るようになるのではないか。 Section FoundationOfSoftwareScience. Lemma e_1_23 : forall A B C : Prop, (A -> B…

Whyツールの習得について( http://groups.google.co.jp/group/fm-forum/browse_thread/thread/6fbd1bc05aa8f999) ということで、 私もやってみた。Whyというのはプログラムの検証用ツールなのだが、 プログラムコードにアサーションのように挿入したWhyのコ…