Coq のカリー・ハワード同型周辺についてメモ.間違いあればご指摘ください. Coq と CoC Coq は元々,Thierry Coquand 氏により提案された Calculus of Constructions (CoC) という型システムの実装として生まれました. その後 CoC は,帰納的データ型などが追加された Calculus of Inductive Constructions (CIC) に拡張され,現在の Coq は CIC の実装となっています. CoC/CIC は,基本的には型システムを定義しただけのものなのですが,実は Coq の証明システムはこの型システムがベース となっています. これは一体どういうことか,次からの節で,直観的な例を通して見ていくことにします. プログラム ≈ 証明 一般に,プログラムの型システムは,次の図みたいな推論木を組み立ててプログラムの