Coq: 定理証明支援系。(プログラムの正当性を機械で示すのを支援) http://coq.inria.fr/で、Coq 入門に良いページ。 http://www.cis.upenn.edu/~bcpierce/sfPENN の大学院向けの授業で、プログラミング言語の礎を教えるために Coq を使ったときの資料。 基礎…

とりあえず、テスト。