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.

The final publication is available at www.degruyter.com
DOI 10.1515/9783110657883-018

Zach-2019-The-Significance-of-the-Curry-Howard-Isomorphism

Download paper

One thought on “The significance of the Curry-Howard isomorphism

Leave a Reply

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