Coqでソフトウェア工学の基礎をいろいろ証明するよという趣旨（多分？）のSoftware Foundationsというウェブ上で読める教科書シリーズがある。 softwarefoundations.cis.upenn.edu 第1巻Logical FoundationsはそのままCoqの教科書になっている。これを読み進…