The significance of the Curry-Howard isomorphism

In Gabriele M. Mras, Paul Weingartner & Bernhard Ritter (eds.), Philosophy of Logic and Mathematics. Proceedings of the 41st International Ludwig Wittgenstein Symposium. Berlin: De Gruyter. pp. 313-326 (2019)

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.

DOI 10.1515/9783110657883-018

Embargoed until November 2020. Please email for offprint.

Leave a Reply

Your email address will not be published. Required fields are marked *