定理証明支援器「Coq」によるプログラミング言語理論の定式化チュートリアル

http://www.cis.upenn.edu/~plclub/popl08-tutorial/

POPLに併設されていたので参加しました。CoqでTAPL序盤（単純型つきλ計算まで）の理論を定義・証明する、という内容。主催者（PennのPLClubの人たち）に聞いたら、先週金曜のカウントで参加登録者67名とのこと。予想は30名程度だったそうなので盛況のようです。

いつも偉そうなことを言っておいてアレなのですが、Coqは話を聞くばかりで、実は触ったことがなかった(!)ので、非常に勉強になりました。隣のA氏（エキスパート）からいろいろと教わりながら聞けたので、さらにナイスでした。:-) さすがに時間不足で説明は駆け足でしたが、ホテルに帰ってから最後（型安全性の証明）まで練習問題をやってみました。カリー・ハワード同型とTAPL序盤程度の知識があれば、上のURLにあるソースコード(coq-tutorial.zip)だけでもコメントやヒントが充実しているので十分にわかるのではないかと思います。

この手の話では変数束縛が最大の問題なのですが、PLClubで作ったCoq用ライブラリを使う形になっていました。テクニカルには"locally nameless representation"（束縛変数はde Bruijn index、自由変数はatomicなシンボルで表現する）を採用していました。名前のfreshnessは「すでに使用されている名前」を渡して保つ"co-finite"方式でした。