Oisomorfismo de Curry–Howard é uma relação direta entre programas de computador e provas matemáticas. Também conhecido como correspondência de Curry–Howard, correspondência provas-como-programas, e correspondência fórmulas-como-tipos, ele se refere à generalização de uma analogia sintática entre sistemas delógica formal e cálculos computacionais que foi descoberto pela primeira vez pelo matemático americanoHaskell Curry e o lógicoWilliam Alvin Howard.

Em primeiro lugar, a correspondência de Curry-Howard é:

1. A observação em 1934 feita porCurry de que tipos de combinadores poderiam ser vistos como esquemas axiomáticos para a lógicaintuicionista implicacional.
2. A observação em 1958 feita porCurry de que certos tipos desistemas de provas, chamados desistemas de Hilbert, coincide em algum fragmento com um fragmento tipado de um modelo computacional conhecido comológica combinatória.
3. A observação em 1969 feita porHoward que outro, mais “alto-nível”, sistema de prova, conhecido comodedução natural, pode ser diretamente interpretado em sua versão intuicionista como uma variante tipada domodelo computacional conhecido comolambda cálculo.

Em outras palavras, a correspondência de Curry-Howard é a observação de que duas famílias de formalismos que pareciam não relacionadas (os sistemas de prova e os modelos computacionais) eram, nos dois exemplos considerados por Curry e Howard, na verdade estruturalmente os mesmos tipos de objetos.

Se agora nos abstrairmos das peculiaridades desse ou daquele formalismo, a generalização imediata é a seguinte: “uma prova é um programa, a formula que ela prova é um tipo para o programa”. Informalmente, isso pode ser visto como umaanalogia que diz que otipo de retorno de uma função (isto é, o tipo dos valores retornados por uma função) é análogo a um teorema lógico, sujeito a hipóteses correspondendo aos tipos dos valores usados na função como argumentos; e que o programa para computar a função é análogo a prova daquele teorema. Isso estabelece uma forma deprogramação lógica em uma base robusta: “provas podem ser representadas como programas, e especialmente temos lambda” ou, em outras palavras, “provas podem ser executadas”.

A correspondência foi o ponto inicial de um grande número de novas pesquisas após sua descoberta, levando a criação de uma nova classe desistemas formais designados a agir tanto como sistemas de prova e como tipos de linguagens deprogramação funcional. Isso inclui ateoria de tipos intuicionista de Martin-Löf e oCálculo de Construções de Coquand, dois tipos de cálculos nos quais provas são objetos comuns do discurso e nos quais um pode dizer propriedades de provas da mesma maneira que é feita em qualquer programa. Esse campo de pesquisa é normalmente chamado deteoria dos tipos moderna.

Esseslambda cálculos tipados derivados do paradigma de Curry-Howard levarem ao desenvolvimento de programas como oCoq, no qual provas, vistas como programas, podem ser formalizadas, verificadas e executadas.

Um direção diferente é usar um programa para extrair uma prova, dada a suacorretude – uma área de pesquisa que está intimamente relacionada acódigo portador-de-prova. Isso somente é factível se alinguagem de programação usada para escrever o programa é ricamente tipada: o desenvolvimento desses tipos de sistemas tem sido parcialmente motivado pelo desejo de fazer a correspondência de Curry-Howard relevante sob um conceito prático.

A correspondência Curry-Howard também levanta novas perguntas em relação ao conteúdo computacional de conceitos de provas que não foram cobertos pelos trabalhos originais de Curry e Howard. Em particular, alógica clássica tem se mostrado correspondente à habilidade de manipular a continuação de programas e a simetria docálculo de sequentes para expressar a dualidade entre duasestratégias de valoração conhecidas como chamada-por-nome e chamada-por-valor.

Especula-se que a correspondência de Curry-Howard pode levar a uma substancial unificação entre a lógica matemática e a base da ciência da computação.

Sistemas de Hilbert e dedução natural são somente dois tipos de sistemas de prova dentre uma grande família de formalismos. Sintaxes alternativas incluem ocálculo de sequentes,redes de prova,cálculo de estruturas, etc. Se admitirmos a correspondência de Curry-Howard como um princípio de que qualquer tipo de sistema de prova esconde um modelo computacional em seu âmago, uma teoria sobre as estruturas computacionais não tipadas subjacentes a esses tipos de provas deve ser possível de existir. Logo, uma questão natural é se alguma coisa matematicamente interessante pode ser dita sobre esses Cálculos Computacionais subjacentes.

Reciprocamente,lógica combinatória elambda calculo simplesmente tipado não são os únicosmodelos computacionais. Alógica linear de Girard foi desenvolvida partindo da análise do uso de recursos de alguns modelos de lambda calculo; podemos imaginar uma versão tipada de umaMáquina de Turing que se comportaria como um sistema de prova?Linguagens assembly tipadas são um exemplo desses modelos de computação “baixo-nível” que contém tipos.

Por causa da possibilidade de escrita de programas que nunca param, modelosTuring-completos de computação (como linguagens comfunções recursivas arbitrárias) devem ser interpretadas com cuidado, pois uma aplicação ingênua da correspondência leva a uma lógica inconsistente. A melhor forma de lidar com computação arbitrária de um ponto de vista lógico é ainda uma questão de pesquisa extremamente debatida, mas uma abordagem popular é baseada no uso demonads para segregar que provavelmente para de código que potencialmente não para (uma abordagem que também generaliza modelos computacionais muito ricos,^[1] e é ela própria relacionada a lógica de modelar por extensão natural do ismorfismo de Curry-Howard^{[ext 1]}). Uma abordagem mais radical, feita porprogramação totalmente funcional, é eliminar recursões sem restrição (e evita a completude de Turing, mas ainda assim mantendo uma complexidade computacional alta), usandoco-recursão mais controlada onde comportamento “não-parável” é na verdade desejável.

Em sua formulação mais geral, a correspondência de Curry-Howard é uma correspondência entreCálculo da Prova formal esistemas de tipos paramodelos computacionais. Em particular, ela é dividida em duas correspondências. Um no nível deformulas etipos que é independente de qual sistema de provas ou modelo computacional é considerada,e outra no nível deprovas eprogramas que, por sua vez, é específica para o sistema de provas e modelo computacional considerado.

No nível de formulas e tipos, a correspondência diz que implicação se comporta como um “tipo função”, conjunção como um tipo “produto” (isso pode ser chamado de tupla, struct, lista ou algum outro termo dependente da linguagem), disjunção como um “tipo soma” (esse tipo pode ser chamado de união, union), a fórmula falsa como o tipo vazio e a fórmula verdade como um tipo conjunto-unitário (cujo único membro é o objeto null). Quantificadores correspondem ao espaço de funções dependentes ou produtos (o que for mais apropriado).

Isso pode ser resumido na seguinte tabela:

No nível de sistemas de prova e modelos computacionais, a correspondência mostra principalmente a identidade da estrutura, primeiramente, entre algumas formulações de sistemas particulares conhecidos como sistemas dededuções de Hilbert elógica combinatória, e, em segundo lugar, entre algumas formulações de sistemas conhecidos comodedução natural elambda cálculo.

Entre o sistema de dedução natural e o lambda calculo, existem as seguintes correspondências:

Foi o início de um simples trecho do livro de Curry e Fey, 1958, sobre lógica combinatória: os tipos mais simples para os combinadores básicos K e S dalógica combinatória surpreendentemente corresponderam com o respectivoesquemas axiomáticos α → (β → α) e (α → (β → γ)) → ((α → β) → (α → γ)) usado nossistemas de Hilbert. Por essa razão, esses esquemas são normalmente chamados axiomas K e S. <-- TODO: Exemplos de programas vistos como provas em uma lógica de Hilbert são dadosabaixo. -->

Se nos restringirmos ao fragmento intuicionístico implicacional, uma maneira simples de formalizar lógica usando um sistema de Hilbert é a seguinte: Seja Γ um conjunto finito de fórmulas, consideradas hipóteses. Dizemos que δ é derivável a partir de Γ, e escrevemos Γ⊢ δ, nos seguintes casos:

• δ é uma hipótese, isto é, ela é uma fórmula de Γ,
• δ é uma instância de um esquema axiomático; isto é, sobre o sistema axiomático mais simples:
  • δ tem a forma α → (β → α), ou
  • δtem a forma (α → (β → γ)) → ((α → β) → (α → γ)),
• δ é gerada por dedução, isto é, para algum α, tanto α → δ como α já são deriváveis a partir de Γ (essa é a regra demodus ponens)

Isso pode ser formalizado usandoregras de inferência, que é o que fazemos na coluna a esquerda da tabela a seguir.

Podemos formular lógica combinatória tipada usando uma sintaxe similar: seja Γ um conjunto finito de variáveis, junto com seus tipos. Um termo T (também junto de seu tipo) vai depender nesses variáveis [Γ⊢ T:δ] quando:

• T é uma das variáveis de Γ,
• T é um combinador básico; i.e., sob a base combinatória mais comum:
  • T é K:α → (β → α) [onde α e β são os tipos de seus argumentos], ou
  • T é S:(α → (β → γ)) → ((α → β) → (α → γ)),
• T é a composição de dois sub-termos que dependem das variáveis em Γ.

As regras de geração definidas aqui são dadas na coluna da direita abaixo. O trecho de Curry diz simplesmente que as duas colunas seguem uma correspondência de um-para-um. A restrição da correspondência para alógica intuicionista significa que algumatautologia dalógica clássica, como aLei de Peirce ((α → β) → α) → α, são excluídas da correspondência.

Lógica intuicionista implicacional de Hilbert	Lógica combinatória simplesmente tipada
${\displaystyle \frac{\alpha \in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢\alpha }\text{Assum}}$	${\displaystyle \frac{x:\alpha \in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢x:\alpha }}$
${\displaystyle \frac{}{\mathrm{\Gamma }⊢\alpha \to (\beta \to \alpha )}{\text{Ax}}_K}$	${\displaystyle \frac{}{\mathrm{\Gamma }⊢K:\alpha \to (\beta \to \alpha )}}$
${\displaystyle \frac{}{\mathrm{\Gamma }⊢(\alpha \to (\beta \to \gamma ))\to ((\alpha \to \beta )\to (\alpha \to \gamma ))}{\text{Ax}}_S}$	${\displaystyle \frac{}{\mathrm{\Gamma }⊢S:(\alpha \to (\beta \to \gamma ))\to ((\alpha \to \beta )\to (\alpha \to \gamma ))}}$
${\displaystyle \frac{\mathrm{\Gamma }⊢\alpha \to \beta \mathrm{\Gamma }⊢\alpha }{\mathrm{\Gamma }⊢\beta }\text{Modus Ponens}}$	${\displaystyle \frac{\mathrm{\Gamma }⊢E_1:\alpha \to \beta \mathrm{\Gamma }⊢E_2:\alpha }{\mathrm{\Gamma }⊢E_1{E}_2:\beta }}$

Vista de um nível mais abstrato, a correspondência pode ser reescrita como mostrada na tabela a seguir. Especialmente, oTeorema da Dedução específico para a lógica de Hilbert corresponde ao processo deEliminação da abstração da lógica combinatória.

Graças à correspondência, resultados da lógica combinatória podem ser transferidos para a lógica de Hilbert e vice-versa. Por exemplo, a noção deredução de termos na lógica combinatória pode ser transferida para a lógica de Hiolbert e ela provê uma maneira de canonicamente transformar uma prova em outra prova de uma mesma sentença. Também pode-se transferir a noção de termos normais para a noção de provas normais, expressando que as hipóteses dos axiomas nunca precisam estar todas desacopladas (já que a simplificação pode acontecer).

Reciprocamente, a improbabilidade da lógica instuicionista daLei de Peirce pode ser transferida de volta para a lógica combinatória: existe nenhum termo tipado da lógica combinatória que tipável com o tipo ((α → β) → α) → α.

Resultados da completude de alguns conjuntos de combinadores ou axiomas também podem ser transferidos. Por exemplo, o fato de que o combinadorX constitui umabase de único ponto da lógica combinatória (extensiva) implica que o única esquema axiomático

(((α → (β → γ)) → ((α → β) → (α → γ))) → ((δ → (ε → δ)) → ζ)) → ζ,

que é otipo principal deX, é um substituto adequado para a combinação dos esquemas aquimáticos

α → (β → α) and

(α → (β → γ)) → ((α → β) → (α → γ)).

Depois deCurry enfatizar a correspondência sintática entre adedução de Hilberte a [lógica combinatória],Howard tornou explícita em 1969 uma analogia sintática entre os programas dolambda cálculo simplesmente tipado e as provas dadedução natural. Abaixo, o lado esquerdo formaliza a implicação intuicionista da dedução natural como um calculo desequentes (o uso de sequentes é um padrão em discussões sobre o isomorfismo de Curry-Howerd pois eles permitem que as regras de dedução sejam escritas mais claramente) com enfraquecimento implícito e o lado direito mostra as regras de tipagem dolambda cálculo. No lado esquerdo, Γ, Γ₁ e Γ₂ denotam sequências ordenadas de fórmulas enquanto no lado direito eles denotam sequências de fórmulas nomeadas (i. e., tipadas) como todos os nomes diferentes.

Implicação intuicionista da dedução natural	Regras de tipagem de lambda cálculo
${\displaystyle \frac{}{{\mathrm{\Gamma }}_1,\alpha ,{\mathrm{\Gamma }}_2⊢\alpha }\text{Ax}}$	${\displaystyle \frac{}{{\mathrm{\Gamma }}_1,x:\alpha ,{\mathrm{\Gamma }}_2⊢x:\alpha }}$
${\displaystyle \frac{\mathrm{\Gamma },\alpha ⊢\beta }{\mathrm{\Gamma }⊢\alpha \to \beta }\to I}$	${\displaystyle \frac{\mathrm{\Gamma },x:\alpha ⊢t:\beta }{\mathrm{\Gamma }⊢\lambda x.t:\alpha \to \beta }}$
${\displaystyle \frac{\mathrm{\Gamma }⊢\alpha \to \beta \mathrm{\Gamma }⊢\alpha }{\mathrm{\Gamma }⊢\beta }\to E}$	${\displaystyle \frac{\mathrm{\Gamma }⊢t:\alpha \to \beta \mathrm{\Gamma }⊢u:\alpha }{\mathrm{\Gamma }⊢tu:\beta }}$

Parafraseando a correspondência, provar Γ⊢ α significa ter um programa que, dados valores com os tipos listados em Γ, construir um objeto do tipo α. Um axioma corresponde à introdução de uma nova variável com um novo, ainda não associado, tipo, a regra →  I corresponde à função abstração e a regra → E corresponde a função aplicação. Observe que a correspondência não é exata se o contexto Γ é tomado como sendo um conjunto de fórmulas pois, por exemplo, os termos-λ λx.λy.x e λx.λy.y do tipo α → α → α não seriam distinguíveis na correspondência. <--TODO: Exemplos são dadosabaixo. -->

Howard mostrou que a correspondência estende-se para outros conectivos da lógica e outras construções do lambda cálculo simplesmente tipado. Visto de um nível abstrato, a correspondência pode então ser resumida como mostrado na tabela a seguir. Especialmente, ela também mostra que a noção de formas normais emlambda cálculo corresponde à noção de dedução normal dePrawitz da dedução natural. Disso deduzimos, entre outras coisas, que os algoritmos para oproblema de habitação de tipos pode ser transformado em algoritmos para decidir a probabilidadeintuicionista.

A correspondência de Howard naturalmente estende-se para outras extensões dadedução natural elambda cálculo simplesmente tipado. Aqui está uma lista pequena:

• Girard-ReynoldsSystem F como uma linguagem comum para tanto a lógica proposicional de segunda ordem para o lambda cálculo polimórfico,
• Lógica de alta ordem e oSistema F_ω de Girard,
• tipos indudivos comotipo algébrico de dados
• necessidade${\displaystyle ◻}$ emlógica de modelos e computação por estágios^{[ext 2]}
• possibilidade${\displaystyle ◊}$ emlógica de modelos e tipos monadicos para efeitos^{[ext 1]}
• O cálculo λ_I correspondente alógica relevante.^[2]
• A modalidade da veracidade local (∇) natopologia Grothendieck ou a equivalente modalidade "lax" (∘) de Benton, Bierman, e de Paiva (1998) correspondem a lógica-CL descrevebti "tipos de computação".^[3]

Referências

• Curry, Haskell (1934), «Functionality in Combinatory Logic»,Proceedings of the National Academy of Sciences,20, pp. 584–590 .
• Curry, Haskell B.; Feys, Robert (1958), Craig, William, ed.,Combinatory Logic Vol. I, Amsterdam: North-Holland , 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. (1980) [original paper manuscript from 1969], «The formulae-as-types notion of construction», in:Seldin, Jonathan P.;Hindley, J. Roger,To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism,ISBN 978-0-12-349050-6, Boston, MA:Academic Press, pp. 479–490 .

• Griffin, Timothy G. (1990), «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, pp. 47–57 .
• Parigot, Michel (1992), «Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction»,Logic Programming and Automated Reasoning: International Conference LPAR '92 Proceedings, St. Petersburg, Russia,ISBN 978-3-540-55727-2, Lecture Notes in Computer Science,624, Berlin; New York:Springer-Verlag, pp. 190–201 .
• Herbelin, Hugo (1995), «A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure», in: Pacholski, Leszek; Tiuryn, Jerzy,Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25–30, 1994, Selected Papers,ISBN 978-3-540-60017-6, Lecture Notes in Computer Science,933, Berlin; New York:Springer-Verlag, pp. 61–75 .
• Gabbay, Dov; de Queiroz, Ruy (1992), «Extending the Curry–Howard interpretation to linear, relevant and other resource logics»,Journal of Symbolic Logic,57, pp. 1319–1365 . (Full version of the paper presented atLogic Colloquium '90, Helsinki. Abstract inJSL 56(3):1139–1140, 1991.)
• de Queiroz, Ruy; Gabbay, Dov (1994), «Equality in Labelled Deductive Systems and the Functional Interpretation of Propositional Equality», in: Dekker, Paul; Stokhof, Martin,Proceedings of the Ninth Amsterdam Colloquium,ISBN 90-74795-07-2, ILLC/Department of Philosophy, University of Amsterdam, pp. 547–565 .
• de Queiroz, Ruy; Gabbay, Dov (1995), «The Functional Interpretation of the Existential Quantifier»,Bulletin of the Interest Group in Pure and Applied Logics, 3(2–3), pp. 243–290 . (Full version of a paper presented atLogic Colloquium '91, Uppsala. Abstract inJSL 58(2):753–754, 1993.)
• de Queiroz, Ruy; Gabbay, Dov (1997), «The Functional Interpretation of Modal Necessity», in: de Rijke, Maarten,Advances in Intensional Logic,ISBN 978-0-7923-4711-8, Applied Logic Series,7,Springer-Verlag, pp. 61–91 .
• de Queiroz, Ruy; Gabbay, Dov (1999), «Labelled Natural Deduction», in: Ohlbach, Hans-Juergen; Reyle, Uwe,Logic, Language and Reasoning. Essays in Honor of Dov Gabbay,ISBN 978-0-7923-5687-5, Trends in Logic,7,Kluwer Acad. Pub., pp. 173–250 .
• de Oliveira, Anjolina; de Queiroz, Ruy (1999), «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, pp. 173–215 . (Full version of a paper presented at2nd WoLLIC'95, Recife. Abstract inJournal of the Interest Group in Pure and Applied Logics 4(2):330–332, 1996.)
• Poernomo, Iman; Crossley, John; Wirsing; Martin (2005) [2005],Adapting Proofs-as-Programs: The Curry–Howard Protocol,ISBN 978-0-387-23759-6, Monographs in Computer Science,Springer , concerns the adaptation of proofs-as-programs program synthesis to coarse-grain and imperative program development problems, via a method the authors call the Curry–Howard protocol. Includes a discussion of the Curry–Howard correspondence from a Computer Science perspective.
• de Queiroz, Ruy J.G.B.; de Oliveira, Anjolina (2011), «The Functional Interpretation of Direct Computations»,Electronic Notes in Theoretical Computer Science,269,Elsevier, pp. 19–40,doi:10.1016/j.entcs.2011.03.003 . (Full version of a paper presented atLSFA 2010, Natal, Brazil.)

• de Queiroz, Ruy J.G.B. (1994),«Normalisation and language-games»,Dialectica,48 (2), pp. 83–123 ^{[ligação inativa]}. (Early version presented atLogic Colloquium '88, Padova. Abstract inJSL 55:425, 1990.)
• de Queiroz, Ruy J.G.B. (2001),«Meaning, function, purpose, usefulness, consequences – interconnected concepts»,Logic Journal of the Interest Group in Pure and Applied Logics,9 (5), pp. 693–734 . (Early version presented atFourteenth International Wittgenstein Symposium (Centenary Celebration) held in Kirchberg/Wechsel, August 13–20, 1989.)
• de Queiroz, Ruy J.G.B. (2008),«On reduction rules, meaning-as-use and proof-theoretic semantics»,Studia Logica,90 (2), pp. 211–247 ^{[ligação inativa]}.

• De Bruijn, Nicolaas Govert (1995),«On the roles of types in mathematics»(PDF), in: Groote, Philippe de,The Curry–Howard isomorphism,ISBN 978-2-87209-363-2, Cahiers du Centre de logique (Université catholique de Louvain),8, Academia-Bruyland, pp. 27–54 , the contribution of de Bruijn by himself.
• Geuvers, Herman (1995), «The Calculus of Constructions and Higher Order Logic», in: Groote, Philippe de,The Curry–Howard isomorphism,ISBN 978-2-87209-363-2, Cahiers du Centre de logique (Université catholique de Louvain),8, Academia-Bruyland, pp. 139–191 , contains a synthetic introduction to the Curry–Howard correspondence.
• Gallier, Jean H. (1995),«On the Correspondence between Proofs and Lambda-Terms»(PDF), in: Groote, Philippe de,The Curry–Howard isomorphism,ISBN 978-2-87209-363-2, Cahiers du Centre de logique (Université catholique de Louvain),8, Academia-Bruyland, pp. 55–138 , contains a synthetic introduction to the Curry–Howard correspondence.

• edited by Ph. de Groote. (1995), De Groote, Philippe, ed.,The Curry–Howard Isomorphism,ISBN 978-2-87209-363-2, Cahiers du Centre de Logique (Université catholique de Louvain),8, Academia-Bruylant , 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ł (2006) [1998],Lectures on the Curry–Howard isomorphism,ISBN 978-0-444-52077-7, Studies in Logic and the Foundations of Mathematics,149,Elsevier Science , 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.
• Thompson, Simon (1991).Type Theory and Functional Programming Addison–Wesley.ISBN 0-201-41667-0.
• Poernomo, Iman; Crossley, John; Wirsing; Martin (2005) [2005],Adapting Proofs-as-Programs: The Curry–Howard Protocol,ISBN 978-0-387-23759-6, Monographs in Computer Science,Springer , concerns the adaptation of proofs-as-programs program synthesis to coarse-grain and imperative program development problems, via a method the authors call the Curry–Howard protocol. Includes a discussion of the Curry–Howard correspondence from a Computer Science perspective.
• F. Binard and A. Felty, "Genetic programming with polymorphic types and higher-order functions." InProceedings of the 10th annual conference on Genetic and evolutionary computation, pages 1187 1194, 2008.[1]
• de Queiroz, Ruy J.G.B.; de Oliveira, Anjolina G.; Gabbay, Dov M. (2011) [2011],The Functional Interpretation of Logical Deduction,ISBN 978-981-4360-95-1, Advances in Logic,5,Imperial College Press / World Scientific .

• P.T. Johnstone, 2002,Sketches of an Elephant, section D4.2 (vol 2) gives acategorical view of "what happens" in the Curry–Howard correspondence.

OWikilivroHaskell tem uma página intituladaThe Curry–Howard isomorphism

• The Curry–Howard Correspondence in Haskell
• The Monad Reader 6: Adventures in Classical-Land: Curry–Howard in Haskell, Pierce's law.

• Teoria dos tipos

• !Artigos com ligações inativas
• !Páginas que usam hiperligações mágicas ISBN