Coq
Coq: 定理証明支援系。(プログラムの正当性を機械で示すのを支援)
http://coq.inria.fr/
で、Coq 入門に良いページ。
http://www.cis.upenn.edu/~bcpierce/sf
PENN の大学院向けの授業で、プログラミング言語の礎を教えるために Coq を使ったときの資料。
基礎から入っていくものの、Curry-Howard Isomorphism、simply typed lambda calculus 等の話を経て、最終的には subtyping まで行く。
ICFP'09 のとき、B.C. Pierce が招待講演でこの授業について話した。
曰く、
from
Theory of PL for PL geeks
to
Software Founsation to the masses
一通り演習問題は解いたものの、一部未完;
いつか終わらせたい。
日記
とりあえず、テスト。