ウィキペディア

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

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2011/11/13 13:36 UTC 版)

(カリー＝ハワード同型 から転送)

プログラミング言語理論と証明論において、カリー＝ハワード同型対応（カリー＝ハワードどうけいたいおう、「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)などとしても知られる）とは、計算機プログラムと数理論理学的証明との間の、直接的な対応関係のことである。