Coq で しりとりの圏を形式化した記事を見つけた。 型によるしりとりの成立判定 - コンピュータってすごいらしい via 完全実装付きでもう一度お送りします、しりとりの圏 - 檜山正幸のキマイラ飼育記すばらしかったので、私もちょっと真似して実装してみた。…

SICPを読んでいたら 検証せよ という問題があったので、Coqで検証してみた。問題はペア構造のチャーチエンコーディングの話。Scheme (untyped λ) に比べて Coq (λC) は型が厳格なので、問題の定式化がちょっと大変だったけど、問題自体は簡単に証明できた。 …