Isomorfismo de Curry-Howard

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
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.

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.

Origem, escopo, e consequências[editar | editar código-fonte]

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 principio 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,[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 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[editar | editar código-fonte]

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
Formula verdadeira tipo unitário
Formula 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[editar | editar código-fonte]

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[editar | editar código-fonte]

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, Γ, Γ1 e Γ2 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:

References[editar | editar código-fonte]

Predefinição:More footnotes

  1. Moggi, Eugenio (1991), "Notions of Computation and Monads", Information and Computation 93 (1), http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf 
  2. Sørenson, Morten; Urzyczyn, Paweł, Lectures on the Curry-Howard Isomorphism, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385 
  3. Goldblatt, "7.6 Grothendieck Topology as Intuitionistic Modality", Mathematical Modal Logic: A Model of its Evolution, pp. 76–81, http://homepages.mcs.vuw.ac.nz/~rob/papers/modalhist.pdf . The "lax" modality referred to is from Benton; Bierman; de Paiva (1998), "Computational types from a logical perspective", Journal of Functional Programming 8: 177–193 

Seminal references[editar | editar código-fonte]

  • 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. (09 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, Boston, MA: Academic Press, pp. 479–490, ISBN 978-0-12-349050-6 .

Extensions of the correspondence[editar | editar código-fonte]

  1. a b Pfenning, Frank; Davies, Rowan (2001), "A Judgmental Reconstruction of Modal Logic", Mathematical Structures in Computer Science 11: 511–540, doi:10.1017/S0960129501003322, http://www.cs.cmu.edu/~fp/papers/mscs00.pdf 
  2. Davies, Rowan; Pfenning, Frank (2001), "A Modal Analysis of Staged Computation", Journal of the ACM 48 (3): 555–604, doi:10.1145/382780.382785, http://www.cs.cmu.edu/~fp/papers/jacm00.pdf 
  • 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, Lecture Notes in Computer Science, 624, Berlin; New York: Springer-Verlag, pp. 190–201, ISBN 978-3-540-55727-2 .
  • 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, Lecture Notes in Computer Science, 933, Berlin; New York: Springer-Verlag, pp. 61–75, ISBN 978-3-540-60017-6 .
  • 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, ILLC/Department of Philosophy, University of Amsterdam, pp. 547–565, ISBN 90-74795-07-2 .
  • 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, Applied Logic Series, 7, Springer-Verlag, pp. 61–91, ISBN 978-0-7923-4711-8 .
  • 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, Trends in Logic, 7, Kluwer Acad. Pub., pp. 173–250, ISBN 978-0-7923-5687-5, http://www.springer.com/philosophy/logic/book/978-0-7923-5687-5 .
  • 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, 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, Monographs in Computer Science, Springer, ISBN 978-0-387-23759-6 , 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[editar | editar código-fonte]

Synthetic papers[editar | editar código-fonte]

Books[editar | editar código-fonte]

  • edited by Ph. de Groote. (1995), De Groote, Philippe, ed., The Curry–Howard Isomorphism, Cahiers du Centre de Logique (Université catholique de Louvain), 8, Academia-Bruylant, 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ł (2006) [1998], Lectures on the Curry–Howard isomorphism, Studies in Logic and the Foundations of Mathematics, 149, Elsevier Science, ISBN 978-0-444-52077-7, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385 , 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, Monographs in Computer Science, Springer, ISBN 978-0-387-23759-6 , 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, Advances in Logic, 5, Imperial College Press / World Scientific, ISBN 978-981-4360-95-1 .

Further reading[editar | editar código-fonte]

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

External links[editar | editar código-fonte]

Wikilivros
O wikilivro Haskell tem uma página intitulada The Curry–Howard isomorphism