![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)是在计算机程序和数学证明之间的紧密联系;这种对应也叫做柯里-霍华德同构、公式为类型对应或命题为类型对应。这是对形式逻辑系统和公式计算(computational calculus)之间符号的相似性的推广。它被认为是由美国数学家哈斯凯尔·柯里和逻辑学家威廉·阿尔文·霍瓦德(William Alvin Howard)独立发现的。
此条目已列出参考资料,但文内引注不足,部分内容的来源仍然不明。 (2019年3月6日) |
![](http://upload.wikimedia.org/wikipedia/commons/thumb/8/8b/Coq_plus_comm_screenshot.jpg/640px-Coq_plus_comm_screenshot.jpg)