今回の発表資料は深町氏作のClojureによるプレゼンツール、L5
(https://github.com/fukamachi/L5)を使用した。便利。
2010年振り返り
https://gist.github.com/729087
今年も本当にありがとうございました。
勉強会は1年間で12回開催。
イベント等発表あり、記事執筆ありといろいろ勉強できました。
来年の勉強会では数学も含めた勉強を展開していきたい。
AwodeyのCategory Theoryとかは質問できる機会が少ないので、
こういう場でみんなでやるのが一番かなと。
あと、「Coqの初心者対応はどうするか」については、
数ヶ月に1回「初心者向け紹介説明」をすることを検討している。
超訳Verified Programming in Guru
https://gist.github.com/729089
前回紹介を受けたGuru(http://code.google.com/p/guru-lang/)
を調べたのでその発表資料。
Guru自体がまだ証明の自動化機能を持っていないので、
そこら辺を強化する方法を作り込まないと実用にならないとの話が出た。
Coq Party(11/27)での話(tmiyaさん)
FM-Forumの生い立ちを話して欲しいということでお話をした。
興味深かったこと
***Haskellのお話
欠陥の発生しない範囲を証明する
数値実験で統計的に把握できたものを厳密に証明
***Coq2**
Coq2Ruby
Coq2Clojure(http://patch-tag.com/r/leque/coq-clojure-ext/home)
Coq2JavaScriptとか
変換時に難しいこと
GC有りでないと辛い
クロージャ（関数が前提。オブジェクトでも代用可能）
型がある言語への出力は難しい(Scalaは難しい)
OCaml : Obj.magic
Haskell : Unsafe**
***extractができれば、別のコミュニティで発表できるよ。
extractのコード読むの楽しそう
***HeXe→{C,ActionScript,OCaml}
Ltac
auto,autorewriteのHint DBに規則を追加する
matchのパターンの並び順が結構難しい。並び順によって違うのにmatchしてしまう。
CPDTには出て来ないけど重要なこと
Function
この関数の値が小さくなっていく（互除法の証明）
Category Theory(Awodey)
P61のzero homomorphismって何？
何してるかは分かるんだけど・・・zero objectなんかと同じで、単位元のように振る舞うものなんではないか。
Types and Programming Language
演習5.3.7
wrongはlambda式ではどう表すの？
その他
Coqでは、証明できないとき、なぜ証明できないのかは分からない
証明できるかどうかを(Alloyなんかで)反例で示してくれるのはありがたいかもしれない。
Compcert Verified Compiler
http://www.cs.uoregon.edu/Activities/summerschool/summer10/curriculum.html
FM-Forumの活動の一つとして、TAPLのサマリを作るか。
"Seven Languages in Seven Weeks"
http://www.pragprog.com/titles/btlang/seven-languages-in-seven-weeks
みんなで持ち回りで発表しようか。
Clojureやりたい(by ken.coba)
