Isomorfismo de Curry-Howard

O isomorfismo 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 de lógica formal e cálculos computacionais que foi descoberto pela primeira vez pelo matemático americano Haskell Curry e o lógico William Alvin Howard.

Uma prova escrita como um programa funcional: a prova de comutatividade da adição de números naturais no assistente de provas Coq. nat_ind está para a indução matemática, eq_ind substitui a igualdade e f_equal toma a mesma função em ambos os lados da igualdade. Teoremas mais atuais são referenciados como mostrado. m = m + 0 and S (m + y) = m + S y.

Origem, escopo, e consequências

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

1. A observação em 1934 feita por Curry de que tipos de combinadores poderiam ser vistos como esquemas axiomáticos para a lógica intuicionista implicacional.
2. A observação em 1958 feita por Curry de que certos tipos de sistemas de provas, chamados de sistemas de Hilbert , coincide em algum fragmento com um fragmento tipado de um modelo computacional conhecido como lógica combinatória.
3. A observação em 1969 feita por Howard que outro, mais “alto-nível”, sistema de prova, conhecido como dedução natural, pode ser diretamente interpretado em sua versão intuicionista como uma variante tipada do modelo computacional conhecido como lambda 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 uma analogia que diz que o tipo 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 de programaçã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 de sistemas formais designados a agir tanto como sistemas de prova e como tipos de linguagens de programação funcional. Isso inclui a teoria de tipos intuicionista de Martin-Löf e o Cá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 de teoria dos tipos moderna.

Esses lambda cálculos tipados derivados do paradigma de Curry-Howard levarem ao desenvolvimento de programas como o Coq, 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 sua corretude – uma área de pesquisa que está intimamente relacionada a código portador-de-prova. Isso somente é factível se a linguagem 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, a lógica clássica tem se mostrado correspondente à habilidade de manipular a continuação de programas e a simetria do cálculo de sequentes para expressar a dualidade entre duas estraté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 o cá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 e lambda calculo simplesmente tipado não são os únicos modelos computacionais. A ló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 uma Má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, modelos Turing-completos de computação (como linguagens com funçõ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 de monads para segregar que provavelmente para de código que potencialmente não para (uma abordagem que também generaliza modelos computacionais muito ricos, e é ela própria relacionada a lógica de modelar por extensão natural do ismorfismo de Curry-Howard ). Uma abordagem mais radical, feita por programação totalmente funcional, é eliminar recursões sem restrição (e evita a completude de Turing, mas ainda assim mantendo uma complexidade computacional alta), usando co-recursão mais controlada onde comportamento “não-parável” é na verdade desejável.

Formulação geral

Em sua formulação mais geral, a correspondência de Curry-Howard é uma correspondência entre Cálculo da Prova formal e sistemas de tipos para modelos computacionais. Em particular, ela é dividida em duas correspondências. Um no nível de formulas e tipos que é independente de qual sistema de provas ou modelo computacional é considerada,e outra no nível de provas e programas 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:

Lado lógico	Lado programacional
Quantificador universal	espaço de função generalizada (tipo Π)
Qualificador existencial	Produto cartesiano generalizado (tipo Σ
implicação	tipo função
conjunção	tipo produto
disjunção	tipo soma
Fórmula verdadeira	tipo unitário
Fórmula falsa	tipo vazio

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 de deduções de Hilbert e lógica combinatória, e, em segundo lugar, entre algumas formulações de sistemas conhecidos como dedução natural e lambda cálculo.

Lado lógico	Lado programacional
Sistema de Hilbert	Sistema de tipos para lógica combinatória
dedução natural	Sistema de tipos para Lambda Cálculo

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

Lado lógico	Lado programacional
hipótese	variável livre
remoção da implicação	aplicação
introdução da implicação	abstração

Correspondência entre os Sistemas de dedução de Hilbert e a lógica combinatória

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 da lógica combinatória surpreendentemente corresponderam com o respectivo esquemas axiomáticos α → (β → α) e (α → (β → γ)) → ((α → β) → (α → γ)) usado nos sistemas 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 dados abaixo. -->

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 de modus ponens)

Isso pode ser formalizado usando regras 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 a lógica intuicionista significa que alguma tautologia da lógica clássica, como a Lei de Peirce ((α → β) → α) → α, são excluídas da correspondência.

Lógica intuicionista implicacional de Hilbert	Lógica combinatória simplesmente tipada
${\frac {\alpha \in \Gamma }{\Gamma \vdash \alpha }}{\text{Assum}}$	${\frac {x:\alpha \in \Gamma }{\Gamma \vdash x:\alpha }}$
${\frac {}{\Gamma \vdash \alpha \rightarrow (\beta \rightarrow \alpha )}}{\text{Ax}}_{K}$	${\frac {}{\Gamma \vdash K:\alpha \rightarrow (\beta \rightarrow \alpha )}}$
${\frac {}{\Gamma \vdash (\alpha \!\rightarrow \!(\beta \!\rightarrow \!\gamma ))\!\rightarrow \!((\alpha \!\rightarrow \!\beta )\!\rightarrow \!(\alpha \!\rightarrow \!\gamma ))}}{\text{Ax}}_{S}$	${\frac {}{\Gamma \vdash S:(\alpha \!\rightarrow \!(\beta \!\rightarrow \!\gamma ))\!\rightarrow \!((\alpha \!\rightarrow \!\beta )\!\rightarrow \!(\alpha \!\rightarrow \!\gamma ))}}$
${\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}{\text{Modus Ponens}}$	${\frac {\Gamma \vdash E_{1}:\alpha \rightarrow \beta \qquad \Gamma \vdash E_{2}:\alpha }{\Gamma \vdash 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, o Teorema da Dedução específico para a lógica de Hilbert corresponde ao processo de Eliminação da abstração da lógica combinatória.

Lado Lógico	Lado Programacional
suposição	variável
axiomas	combinadores
modus ponens	aplicações
Teorema da Dedução	Eliminação da abstração

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 de reduçã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 da Lei 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 combinador X constitui uma base de único ponto da lógica combinatória (extensiva) implica que o única esquema axiomático

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

que é o tipo principal de X, é um substituto adequado para a combinação dos esquemas aquimáticos

α → (β → α) and

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

Correspondência entre dedução natural e lambda cálculo

Depois de Curry enfatizar a correspondência sintática entre a dedução de Hilbert e a [lógica combinatória], Howard tornou explícita em 1969 uma analogia sintática entre os programas do lambda cálculo simplesmente tipado e as provas da dedução natural. Abaixo, o lado esquerdo formaliza a implicação intuicionista da dedução natural como um calculo de sequentes (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 do lambda 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
${\frac {}{\Gamma _{1},\alpha ,\Gamma _{2}\vdash \alpha }}{\text{Ax}}$	${\frac {}{\Gamma _{1},x:\alpha ,\Gamma _{2}\vdash x:\alpha }}$
${\frac {\Gamma ,\alpha \vdash \beta }{\Gamma \vdash \alpha \rightarrow \beta }}\rightarrow I$	${\frac {\Gamma ,x:\alpha \vdash t:\beta }{\Gamma \vdash \lambda x.t:\alpha \rightarrow \beta }}$
${\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}\rightarrow E$	${\frac {\Gamma \vdash t:\alpha \rightarrow \beta \qquad \Gamma \vdash u:\alpha }{\Gamma \vdash t\;u:\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 dados abaixo. -->

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 em lambda cálculo corresponde à noção de dedução normal de Prawitz da dedução natural. Disso deduzimos, entre outras coisas, que os algoritmos para o problema de habitação de tipos pode ser transformado em algoritmos para decidir a probabilidade intuicionista.

Lado Lógico	Lado Programacional
axioma	variável
regra de introdução	construtor
regra de eliminação	destrutor
dedução normal	forma normal
normalização de deduções	normalização fraca
provabilidade	problema de habitação de tipos
tautologia intuicionista	tipo habitado

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

• Girard-Reynolds System 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 o Sistema F_ω de Girard,
• tipos indudivos como tipo algébrico de dados
• necessidade $\Box$ em lógica de modelos e computação por estágios
• possibilidade $\Diamond$ em lógica de modelos e tipos monadicos para efeitos
• O cálculo λ_I correspondente a lógica relevante.
• A modalidade da veracidade local (∇) na topologia Grothendieck ou a equivalente modalidade "lax" (∘) de Benton, Bierman, e de Paiva (1998) correspondem a lógica-CL descrevebti "tipos de computação".

Referências

Seminal references

• 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 .

Extensions of the correspondence

• 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 at Logic Colloquium '90, Helsinki. Abstract in JSL 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 at Logic Colloquium '91, Uppsala. Abstract in JSL 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 at 2nd WoLLIC'95, Recife. Abstract in Journal 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 at LSFA 2010, Natal, Brazil.)

Philosophical interpretations

• de Queiroz, Ruy J.G.B. (1994), «Normalisation and language-games», Dialectica, 48 (2), pp. 83–123 ^{[ligação inativa]}. (Early version presented at Logic Colloquium '88, Padova. Abstract in JSL 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 at Fourteenth 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]}.

Synthetic papers

• 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.

Livros

• 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." In Proceedings 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 .

Mais leitura

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

Ligações externas

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