The Significance of the Curry-Howard Isomorphism

Date
2019-11-19
Journal Title
Journal ISSN
Volume Title
Publisher
De Gruyter
Abstract
The Curry-Howard isomorphism is a proof-theoretic result that establishes a connection between derivations in natural deduction and terms in typed lambda calculus. It is an important proof-theoretic result, but also underlies the development of type systems for programming languages. This fact suggests a potential importance of the result for a philosophy of code.
Description
Keywords
Citation
Zach, R. (2019). The Significance of the Curry-Howard Isomorphism, "Proceedings of the 41st International Ludwig Wittgenstein Symposium". Berlin: De Gruyter. pp. 313-326 (2019). DOI 10.1515/9783110657883-018