The significance of the Curry-Howard isomorphism

Zach, Richard. 2019. “The Significance of the Curry-Howard Isomorphism.” In Philosophy of Logic and Mathematics. Proceedings of the 41st International Ludwig Wittgenstein Symposium, edited by Gabriele M. Mras, Paul Weingartner, and Bernhard Ritter, 313–25. Publications of the Austrian Ludwig Wittgenstein Society, New Series 26. Berlin: De Gruyter. https://doi.org/10.1515/9783110657883-018.

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.

Continue reading