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

一通り演習問題は解いたものの、一部未完;
いつか終わらせたい。