The Significance of the Curry-Howard Isomorphism

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

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.

Categories

Keywords

Reprint years

DOI

10.1515/9783110657883-018

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,628

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

The Curry-Howard isomorphism.Philippe De Groote (ed.) - 1995 - Louvain-la-Neuve: Academia.
Basic theory of functionality. Analogies with propositional algebra.H. B. Curry & R. Feys - 1995 - In Philippe De Groote (ed.), The Curry-Howard Isomorphism. Academia.
Lambda Calculus and Intuitionistic Linear Logic.Simona Ronchi Della Rocca & Luca Roversi - 1997 - Studia Logica 59 (3):417-448.
Lectures on the Curry-Howard isomorphism.Morten Heine Sørensen - 2007 - Boston: Elsevier. Edited by Paweł Urzyczyn.
The formulæ-as-types notion of construction.W. A. Howard - 1995 - In Philippe De Groote (ed.), The Curry-Howard Isomorphism. Academia.
On the roles of types in mathematics.N. G. de Bruijn - 1995 - In Philippe De Groote (ed.), The Curry-Howard Isomorphism. Academia. pp. 27-54.
Linear logic : A survey.J.-Y. Girard - 1995 - In Philippe De Groote (ed.), The Curry-Howard Isomorphism. Academia.
On the correspondence between proofs and lamba-terms.J. Gallier - 1995 - In Philippe De Groote (ed.), The Curry-Howard Isomorphism. Academia.
Realizability, set theory and term extraction.J. Lipton - 1995 - In Philippe De Groote (ed.), The Curry-Howard Isomorphism. Academia. pp. 8--257.
Adding logic to the toolbox of molecular biology.Giovanni Boniolo, Marcello D’Agostino, Mario Piazza & Gabriele Pulcini - 2015 - European Journal for Philosophy of Science 5 (3):399-417.
On the Formulae-as-types Correspondence for Classical Logic.Charles Alexander Stewart - 2000
How far to extend the Curry-Howard isomorphism?Enrico Monconi - 2001 - In V. Fano, M. Stanzione & G. Tarozzi (eds.), Prospettive Della Logica E Della Filosofia Della Scienza. Rubettino. pp. 57.
The completeness of Heyting first-order logic.W. W. Tait - 2003 - Journal of Symbolic Logic 68 (3):751-763.
Curry-Howard terms for linear logic.Frank A. Bäuerle, David Albrecht, John N. Crossley & John S. Jeavons - 1998 - Studia Logica 61 (2):223-235.
Two Flavors of Curry’s Paradox.Jc Beall & Julien Murzi - 2013 - Journal of Philosophy 110 (3):143-165.

Analytics

Added to PP
2019-12-09

Downloads
515 (#35,776)

6 months
16 (#154,237)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Richard Zach
University of Calgary

Citations of this work

Logic in mathematics and computer science.Richard Zach - forthcoming - In Filippo Ferrari, Elke Brendel, Massimiliano Carrara, Ole Hjortland, Gil Sagi, Gila Sher & Florian Steinberger (eds.), Oxford Handbook of Philosophy of Logic. Oxford, UK: Oxford University Press.

Add more citations

References found in this work

No references found.

Add more references