Curry, Haskell, Functionality in Combinatory Logic, Proceedings of the National Academy of Sciences 20: 584–590, 1934.
Curry, Haskell B.; Feys, Robert, Combinatory Logic Vol. I, William Craig, Amsterdam: North-Holland, 1958, with 2 sections by William Craig, see paragraph 9E.
De Bruijn, Nicolaas (1968), Automath, a language for mathematics, Department of Mathematics, Eindhoven University of Technology, TH-report 68-WSK-05. Reprinted in revised form, with two pages commentary, in: Automation and Reasoning, vol 2, Classical papers on computational logic 1967-1970, Springer Verlag, 1983, pp. 159-200.
Howard, William A., The formulae-as-types notion of construction, Seldin, Jonathan P.; Hindley, J. Roger (編), to H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Boston, MA: Academic Press: 479–490, 1980年9月 [1969], ISBN 978-0-12-349050-6 (original manuscript from 1969).
對應的擴展
Griffin, Timothy G., The Formulae-as-Types Notion of Control, Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL '90, San Francisco, CA, USA, 17-19 Jan 1990: 47–57, 1990.
Parigot, Michel, Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction, Logic Programming and Automated Reasoning: International Conference LPAR '92 Proceedings, St. Petersburg, Russia, Lecture Notes in Computer Science 624, Berlin, New York: Springer-Verlag: 190–201, 1992, ISBN 978-3-540-55727-2.
Herbelin, Hugo, A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure, Pacholski, Leszek; Tiuryn, Jerzy (編), Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, Lecture Notes in Computer Science 933, Springer-Verlag: 61–75, 1995, ISBN 978-3-540-60017-6.
Gabbay, Dov; de Queiroz, Ruy, Extending the Curry-Howard interpretation to linear, relevant and other resource logics, Journal of Symbolic Logic 57: 1319–1365, 1992. (Full version of the paper presented at Logic Colloquium '90, Helsinki. Abstract in JSL 56(3):1139-1140, 1991.)
de Queiroz, Ruy; Gabbay, Dov, Equality in Labelled Deductive Systems and the Functional Interpretation of Propositional Equality, Dekker, Paul; Stokhof, Martin (編), Proceedings of the Ninth Amsterdam Colloquium, ILLC/Department of Philosophy, University of Amsterdam: 547–565, 1994, ISBN 9074795072.
de Queiroz, Ruy; Gabbay, Dov, The Functional Interpretation of the Existential Quantifier, Bulletin of the Interest Group in Pure and Applied Logics 3(2–3): 243–290, 1995. (Full version of a paper presented at Logic Colloquium '91, Uppsala. Abstract in JSL 58(2):753-754, 1993.)
de Queiroz, Ruy; Gabbay, Dov, The Functional Interpretation of Modal Necessity, de Rijke, Maarten (編), Advances in Intensional Logic, Applied Logic Series 7, Springer-Verlag: 61–91, 1997, ISBN 978-0-7923-4711-8.
de Oliveira, Anjolina; de Queiroz, Ruy, A Normalization Procedure for the Equational Fragment of Labelled Natural Deduction, Logic Journal of the Interest Group in Pure and Applied Logics 7(2), Oxford Univ Press: 173–215, 1999. (Full version of a paper presented at 2nd WoLLIC'95, Recife. Abstract in Journal of the Interest Group in Pure and Applied Logics 4(2):330-332, 1996.)
綜合性論文
De Bruijn, Nicolaas Govert, On the roles of types in mathematics(PDF), Groote, Philippe de (編), The Curry-Howard isomorphism, Cahiers du Centre de logique (Université catholique de Louvain) 8, Academia-Bruyland: 27–54, [2008-08-28], ISBN 978-2-87209-363-2, (原始內容存檔(PDF)於2021-03-06), the contribution of de Bruijn by himself.
Geuvers, Herman, The Calculus of Constructions and Higher Order Logic, Groote, Philippe de (編), The Curry-Howard isomorphism, Cahiers du Centre de logique (Université catholique de Louvain) 8, Academia-Bruyland: 139–191, ISBN 978-2-87209-363-2, contains a synthetic introduction to the Curry-Howard correspondence.
Gallier, Jean H., On the Correspondence between Proofs and Lambda-Terms(PDF), Groote, Philippe de (編), The Curry-Howard isomorphism, Cahiers du Centre de logique (Université catholique de Louvain) 8, Academia-Bruyland: 55–138, ISBN 978-2-87209-363-2, contains a synthetic introduction to the Curry-Howard correspondence.
書籍
De Groote, Philippe (編), The Curry-Howard Isomorphism, Cahiers du Centre de Logique (Université catholique de Louvain) 8, Academia-Bruylant, 1995, ISBN 978-2-87209-363-2, reproduces the seminal papers of Curry-Feys and Howard, a paper by de Bruijn and a few other papers.
Sörensen, Morten Heine; Urzyczyn, Paweł, Lectures on the Curry-Howard isomorphism, Studies in Logic and the Foundations of Mathematics 149, Elsevier Science, 2006 [1998], ISBN 978-0-44452-077-7, notes on proof theory and type theory, that includes a presentation of the Curry-Howard correspondence, with a focus on the formulae-as-types correspondence
Girard, Jean-Yves (1987-90). Proof and Types (頁面存檔備份,存於網際網路檔案館). Translated by and with appendices by Lafont, Yves and Taylor, Paul. Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7), ISBN 0-521-37181-3, notes on proof theory with a presentation of the Curry-Howard correspondence.