カリー＝ハワード同型対応 - Wikipedia

関数型プログラムとして書かれた証明：自然数の加法に関する交換律のCoqによる証明。 カリー＝ハワード同型対応（カリー＝ハワードどうけいたいおう、英語: Curry–Howard correspondence）とは、プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者ウィリアム・アルヴィン・ハワード（英語版）により最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作

[hamamuratakuo]

「ランベック計算」　カリー＝ハワード＝ランベック対応　ヨアヒム・ランベックは1970年始めに直観主義命題論理とデカルト閉圏の等式理論と対応するある種の型付きコンビネータとの対応関係の証明を示した。

[kinoko_atama]

カリー＝ハワード同型対応 - Wikipedia 参考文献に論文名がいろいろ出ているのnice