Extraction Language Scheme

SICPのEx 2.4 をCoqで解いてみた

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