![cover image](https://wikiwandv2-19431.kxcdn.com/_next/image?url=https://upload.wikimedia.org/wikipedia/commons/thumb/8/8b/Coq_plus_comm_screenshot.jpg/640px-Coq_plus_comm_screenshot.jpg&w=640&q=50)
カリー=ハワード同型対応
ウィキペディア フリーな encyclopedia
カリー=ハワード同型対応(カリー=ハワードどうけいたいおう、英語: Curry–Howard correspondence)とは、プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム=証明」(proofs-as-programs)・「型=命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者ウィリアム・アルヴィン・ハワード(英語版)により最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作的解釈の一種(ブラウワー=ハイティング= コルモゴロフ解釈(BHK 解釈)(英語版))と関係している。[要出典]
![Thumb image](http://upload.wikimedia.org/wikipedia/commons/thumb/8/8b/Coq_plus_comm_screenshot.jpg/640px-Coq_plus_comm_screenshot.jpg)