Mostrar código-fonte de Isomorfismo de Curry-Howard

[[Image:Coq plus comm screenshot.jpg|thumb|300px|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''&nbsp;=&nbsp;''m''&nbsp;+&nbsp;0 and S&nbsp;(''m''&nbsp;+&nbsp;''y'')&nbsp;=&nbsp;''m''&nbsp;+&nbsp;S&nbsp;''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 ==

Em primeiro lugar, a correspondência de Curry-Howard é:
# A observação em 1934 feita por [[Haskell Curry|Curry]]  de que tipos de combinadores poderiam ser vistos como esquemas axiomáticos para a lógica [[intuicionismo|intuicionista]] implicacional.
# A observação em 1958 feita por [[Haskell Curry|Curry]] de que certos tipos de [[sistema de prova|sistemas de provas]], chamados de [[sistema de hilbert|sistemas de Hilbert]], coincide em algum fragmento com um fragmento tipado de um modelo computacional conhecido como [[lógica combinatória]].
# A observação em 1969 feita por [[William Alvin Howard|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 [[Sistema Formal|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álculo]]s 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égia de Valoração|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 [[modelo computacional|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? [[Linguagem Assembly Tipada|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-completo]]s de computação (como linguagens com [[Recursão|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 [[monad]]s para segregar que provavelmente para de código que potencialmente não para (uma abordagem que também generaliza modelos computacionais muito ricos,<ref>{{Citation|primeiro =Eugenio|último =Moggi|ano=1991|título=Notions of Computation and Monads|periódico=Information and Computation|volume=93|número=1|url=http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf}}</ref> e é ela própria relacionada a lógica de modelar por extensão natural do ismorfismo de Curry-Howard<ref name=PfenningDaviesJudgmental group=ext/>). 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 [[Sistema de tipos|sistemas de tipos]] para [[Modelo Computacional|modelos computacionais]]. Em particular, ela é dividida em duas correspondências. Um no nível de [[formula (Lógica Matemática)|formulas]] e [[tipo de dados|tipos]] que é independente de qual sistema de provas ou modelo computacional é considerada,e outra no nível de [[prova matemática|provas]] e [[programa de computador|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:

{| class="wikitable" style="margin: 0 auto; text-align: center;"
! style="width:300px" | Lado lógico
! style="width:300px" | Lado programacional
|-
| [[quantificador universal]] || espaço de função generalizada (tipo Π)
|-
| [[qualificador existencial]] || produto cartesiano generalizado (tipo Σ)
|-
| [[Implicação Lógica|implicação]] || tipo função
|-
| [[Conjunção Lógica|conjunção]] || tipo produto
|-
| [[Disjunção Lógica|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 [[Sistema de Hilbert|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]].

{| class="wikitable" style="margin: 0 auto; text-align: center;"
! style="width:300px" | Lado lógico
! style="width:300px" | 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:

{| class="wikitable" style="margin: 0 auto; text-align: center;"
! style="width:300px" | Lado lógico
! style="width:300px" | Lado programacional
|-
| [[hipótese]] || variável livre
|-
| [[modus ponens|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 [[esquema axiomático|esquemas axiomáticos]] α → (β → α) e (α → (β → γ)) → ((α → β) → (α → γ)) usado nos [[Sistema de Hilber|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 [[#Examples|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 Γ {{Unicode|⊢}} δ, 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 [Γ {{Unicode|⊢}} 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.

{| style="text-align:center; margin: 0 auto;" class="wikitable"
! width="200px"| Lógica intuicionista implicacional de Hilbert
! width="200px"| Lógica combinatória simplesmente tipada
|- style="height:70px" valign=bottom
| <math>\frac{\alpha \in \Gamma}{\Gamma \vdash \alpha} \text{Assum}</math>
| <math>\frac{x:\alpha \in \Gamma}{\Gamma \vdash x:\alpha}</math>
|- style="height:70px" valign=bottom
| <math>\frac{}{\Gamma \vdash \alpha \rightarrow (\beta \rightarrow \alpha)} \text{Ax}_K</math>
| <math>\frac{}{\Gamma \vdash K: \alpha \rightarrow (\beta \rightarrow \alpha)}</math>
|- style="height:70px" valign=bottom
| <math>\frac{}{\Gamma \vdash (\alpha\!\rightarrow\!(\beta\!\rightarrow\!\gamma))\!\rightarrow\!((\alpha\!\rightarrow\!\beta)\!\rightarrow\!(\alpha\!\rightarrow\!\gamma))}\text{Ax}_S</math>
| <math>\frac{}{\Gamma \vdash S: (\alpha\!\rightarrow\!(\beta\!\rightarrow\!\gamma))\!\rightarrow\!((\alpha\!\rightarrow\!\beta)\!\rightarrow\!(\alpha\!\rightarrow\!\gamma))}</math>
|- style="height:70px" valign=bottom
| <math>\frac{\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha}{\Gamma \vdash \beta}\text{Modus Ponens}</math>
| <math>\frac{\Gamma \vdash E_1:\alpha \rightarrow \beta \qquad \Gamma \vdash E_2:\alpha}{\Gamma \vdash E_1\;E_2:\beta} </math>
|}

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.

{| class="wikitable" style="margin: 0 auto; text-align: center;"
! style="width:200px" | Lado Lógico
! style="width:200px" | 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 [[Combinatory logic#One-point basis|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 [[Haskell Curry|Curry]] enfatizar a correspondência sintática entre a [[Sistemas de Hilbert|dedução de Hilbert]]
e a [lógica combinatória], [[William Alvin Howard|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 [[sequente]]s (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, Γ, Γ<sub>1</sub> e Γ<sub>2</sub> 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.

<br>
{| class="wikitable" style="text-align:center; margin: 0 auto;" cellpadding="10"
! width="200px"| Implicação intuicionista da dedução natural
! width="200px"| Regras de tipagem de lambda cálculo
|- style="height:70px" valign=bottom
| <math>\frac{}{\Gamma_1, \alpha, \Gamma_2 \vdash \alpha} \text{Ax}</math>
| <math>\frac{}{\Gamma_1, x:\alpha, \Gamma_2 \vdash x:\alpha}</math>
|- style="height:70px" valign=bottom
| <math>\frac{\Gamma, \alpha \vdash \beta}{\Gamma \vdash \alpha \rightarrow \beta} \rightarrow I</math>
| <math>\frac{\Gamma, x:\alpha \vdash t:\beta}{\Gamma \vdash \lambda x.t : \alpha \rightarrow \beta}</math>
|- style="height:70px" valign=bottom
| <math>\frac{\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha}{\Gamma \vdash \beta} \rightarrow E</math>
| <math>\frac{\Gamma \vdash t:\alpha \rightarrow \beta \qquad \Gamma \vdash u:\alpha}{\Gamma \vdash t\;u:\beta} </math>
|}

Parafraseando a correspondência, provar Γ {{Unicode|⊢}} α 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 →&nbsp; I  corresponde à função abstração e a regra →&nbsp;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 [[#Examples|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 [[Dag Prawitz|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 [[intuicionismo|intuicionista]].

{| class="wikitable" style="margin: 0 auto; text-align: center;"
! style="width:200px" | Lado Lógico
! style="width:200px" | 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 (lambda cálculo)|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|Sistema F<sub>ω</sub>]] de Girard,
* tipos indudivos como [[tipo algébrico de dados]]
* necessidade <math>\Box</math> em [[lógica de modelos]] e computação por estágios<ref name=DaviesPfenningStaged group=ext>{{Citation|doi=10.1145/382780.382785|primeiro =Rowan|último =Davies|primeiro2 =Frank|último2 =Pfenning|ano=2001|título=A Modal Analysis of Staged Computation|periódico=Journal of the ACM |volume=48|número=3|páginas=555–604|url=http://www.cs.cmu.edu/~fp/papers/jacm00.pdf}}</ref>
* possibilidade <math>\Diamond</math> em [[lógica de modelos]] e tipos monadicos para efeitos<ref name=PfenningDaviesJudgmental group=ext/>
* O cálculo λ<sub>I</sub> correspondente a [[lógica relevante]].<ref>{{Citation|primeiro =Morten|último =Sørenson|primeiro2 =Paweł|último2 =Urzyczyn|título=Lectures on the Curry-Howard Isomorphism|url=http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385}}</ref>
* A modalidade da veracidade local (∇) na [[topologia Grothendieck]] ou a equivalente modalidade "lax" (∘)<!-- should be a large circle --> de Benton, Bierman, e de Paiva (1998) correspondem a lógica-CL descrevebti "tipos de computação".<ref>{{Citation|último =Goldblatt|título=Mathematical Modal Logic: A Model of its Evolution|capítulo=7.6 Grothendieck Topology as Intuitionistic Modality|páginas=76–81|url=http://homepages.mcs.vuw.ac.nz/~rob/papers/modalhist.pdf}}. The "lax" modality referred to is from {{Citation|último =Benton|último2 =Bierman|último3 =de Paiva|título=Computational types from a logical perspective|periódico=Journal of Functional Programming|volume=8|páginas=177–193|ano=1998}}</ref>

{{Referências}}

=== Referências seminais ===
* {{Citation |último1 =Curry |primeiro1 =Haskell |título=Proceedings of the National Academy of Sciences |capítulo=Functionality in Combinatory Logic |ano=1934  | volume=20 |páginas=584–590}}.
* <cite id="CurryFeys_paragraph9E">{{Citation |último1 =Curry |primeiro1 =Haskell B. |último2 =Feys |primeiro2 =Robert |editor-sobrenome1 =Craig |editor-nome1 =William |título=Combinatory Logic Vol. I |publicado=North-Holland |local=Amsterdam |ano=1958}}, with 2 sections by William Craig, see paragraph 9E</cite>. <!-- How to explain to the citing mechanism to tell that William Craig wrote two sections of the book? -->
* 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.&nbsp;159–200.
* {{Citation |último1 =Howard |primeiro1 =William A.
 |capítulo=The formulae-as-types notion of construction
 |páginas=479–490
 |editor-sobrenome1 =Seldin |editor-nome1 =Jonathan P.
 | editor1-link=Jonathan P. Seldin
 |editor-sobrenome2 =Hindley |editor-nome2 =J. Roger
 | editor2-link=J. Roger Hindley
 |título=To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism
 |anooriginal=original paper manuscript from 1969
 |publicado=[[Academic Press]] |local=Boston, MA | isbn=978-0-12-349050-6 |mês=09 |ano=1980}}. <!-- How to explain to the citing mechanism to tell that the paper had remained unpublished from 1969 to 1980? -->

=== Extensões da correspondência ===

<references group=ext>refs=<ref name=PfenningDaviesJudgmental group=ext>{{Citation|primeiro =Frank|último =Pfenning|primeiro2 =Rowan|último2 =Davies|título=A Judgmental Reconstruction of Modal Logic|periódico=Mathematical Structures in Computer Science|volume=11|páginas=511–540|ano=2001|url=http://www.cs.cmu.edu/~fp/papers/mscs00.pdf|doi=10.1017/S0960129501003322}}</ref> </references>
* {{Citation |último1 =Griffin |primeiro1 =Timothy G. |título=Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL '90, San Francisco, CA, USA, 17–19 Jan 1990 |ano=1990 |capítulo=The Formulae-as-Types Notion of Control |páginas=47–57}}.
* {{Citation |último1 =Parigot |primeiro1 =Michel |título=Logic Programming and Automated Reasoning: International Conference LPAR '92 Proceedings, St. Petersburg, Russia |publicado=[[Springer-Verlag]] |local=Berlin; New York | series=Lecture Notes in Computer Science | isbn=978-3-540-55727-2 |ano=1992 | volume=624 |capítulo=Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction |páginas=190–201}}.
* {{Citation |último1 =Herbelin |primeiro1 =Hugo |editor-sobrenome1 =Pacholski |editor-nome1 =Leszek |editor-sobrenome2 =Tiuryn|editor-nome2 =Jerzy  |título=Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25–30, 1994, Selected Papers |publicado=[[Springer-Verlag]] |local=Berlin; New York | series=Lecture Notes in Computer Science | isbn= 978-3-540-60017-6 |ano=1995 | volume=933  |capítulo=A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure |páginas=61–75}}.
* {{Citation |último1 =Gabbay |primeiro1 =Dov |último2 =de Queiroz |primeiro2 =Ruy |título=Journal of Symbolic Logic |capítulo=Extending the Curry–Howard interpretation to linear, relevant and other resource logics |ano=1992  | volume=57 |páginas=1319–1365}}. (Full version of the paper presented at ''Logic Colloquium '90'', Helsinki. Abstract in ''JSL'' 56(3):1139–1140, 1991.)
* {{Citation |último1 =de Queiroz |primeiro1 =Ruy |último2 =Gabbay |primeiro2 =Dov |editor-sobrenome1 =Dekker |editor-nome1 =Paul |editor-sobrenome2 =Stokhof |editor-nome2 =Martin |título=Proceedings of the Ninth Amsterdam Colloquium |capítulo=Equality in Labelled Deductive Systems and the Functional Interpretation of Propositional Equality |ano=1994|publicado=ILLC/Department of Philosophy, University of Amsterdam  | isbn=90-74795-07-2 |páginas=547–565}}.
* {{Citation |último1 =de Queiroz |primeiro1 =Ruy |último2 =Gabbay |primeiro2 =Dov |título=Bulletin of the Interest Group in Pure and Applied Logics |capítulo=The Functional Interpretation of the Existential Quantifier |ano=1995  | volume=3(2–3) |páginas=243–290}}. (Full version of a paper presented at ''Logic Colloquium '91'', Uppsala. Abstract in ''JSL'' 58(2):753–754, 1993.)
* {{Citation |último1 =de Queiroz |primeiro1 =Ruy |último2 =Gabbay |primeiro2 =Dov |editor-sobrenome1 =de Rijke |editor-nome1 =Maarten |título=Advances in Intensional Logic |capítulo=The Functional Interpretation of Modal Necessity | isbn=978-0-7923-4711-8 |ano=1997|publicado=[[Springer-Verlag]]  |series=Applied Logic Series | volume=7 |páginas=61–91}}.
* {{Citation |último1 =de Queiroz |primeiro1 =Ruy |último2 =Gabbay |primeiro2 =Dov |editor-sobrenome1 =Ohlbach |editor-nome1 =Hans-Juergen |editor-sobrenome2 =Reyle |editor-nome2 =Uwe |título=Logic, Language and Reasoning. Essays in Honor of Dov Gabbay  | url=http://www.springer.com/philosophy/logic/book/978-0-7923-5687-5 |publicado=[[Kluwer Acad. Pub.]] | series=Trends in Logic | isbn=978-0-7923-5687-5 |ano=1999 | volume=7 |capítulo=Labelled Natural Deduction |páginas=173–250}}.
* {{Citation |último1 =de Oliveira |primeiro1 =Anjolina |último2 =de Queiroz |primeiro2 =Ruy |título=Logic Journal of the Interest Group in Pure and Applied Logics |capítulo=A Normalization Procedure for the Equational Fragment of Labelled Natural Deduction |publicado=[[Oxford Univ Press]] |ano=1999  | volume=7 |páginas=173–215 |número=2}}. (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.)
* {{citation |último1 =Poernomo |primeiro1 =Iman |último2 =Crossley |primeiro2 =John |último3 =Wirsing |último4 =Martin |título=Adapting Proofs-as-Programs: The Curry–Howard Protocol |publicado=[[Springer Science+Business Media|Springer]] |ano=2005 |anooriginal=2005 | isbn=978-0-387-23759-6 | series=Monographs in Computer Science}}, 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.
* {{Citation |último1 =de Queiroz |primeiro1 =Ruy J.G.B. |último2 =de Oliveira |primeiro2 =Anjolina |título=Electronic Notes in Theoretical Computer Science |capítulo=The Functional Interpretation of Direct Computations | doi=10.1016/j.entcs.2011.03.003 |publicado=[[Elsevier]] |ano=2011  | volume=269 |páginas=19–40}}. (Full version of a paper presented at ''LSFA 2010'', Natal, Brazil.)

=== Interpretações filosóficas ===
* {{Citation |último1=de Queiroz |primeiro1=Ruy J.G.B. |título=Dialectica |capítulo=Normalisation and language-games |capítulourl=http://www3.interscience.wiley.com/journal/119262585/abstract?CRETRY=1&SRETRY=0 |ano=1994 |volume=48 |páginas=83–123 |número=2 }}{{Ligação inativa|data=abril de 2021 }}. (Early version presented at ''Logic Colloquium '88'', Padova. Abstract in ''JSL'' 55:425, 1990.)
* {{Citation |último1 =de Queiroz |primeiro1 =Ruy J.G.B. |título=Logic Journal of the Interest Group in Pure and Applied Logics |capítulo=Meaning, function, purpose, usefulness, consequences – interconnected concepts |capítulourl=http://jigpal.oxfordjournals.org/cgi/content/abstract/9/5/693 |ano=2001  | volume=9 |páginas=693–734 |número=5}}. (Early version presented at ''Fourteenth International Wittgenstein Symposium (Centenary Celebration)'' held in Kirchberg/Wechsel, August 13–20, 1989.)
* {{Citation |último1=de Queiroz |primeiro1=Ruy J.G.B. |título=Studia Logica |capítulo=On reduction rules, meaning-as-use and proof-theoretic semantics |capítulourl=http://www.springerlink.com/content/27nk266126k817gq/ |ano=2008 |volume=90 |páginas=211–247 |número=2 }}{{Ligação inativa|data=abril de 2021 }}.

=== Artigos ===
* {{Citation |último1 =De Bruijn |primeiro1 =Nicolaas Govert |editor-sobrenome1 =Groote |editor-nome1 =Philippe de |título=The Curry–Howard isomorphism |publicado=Academia-Bruyland | series=Cahiers du Centre de logique (Université catholique de Louvain) | isbn=978-2-87209-363-2 | volume=8 |capítulo=On the roles of types in mathematics |capítulourl=http://alexandria.tue.nl/repository/freearticles/597627.pdf |páginas=27–54 |ano=1995}}, the contribution of de Bruijn by himself.
*{{Citation |último1 =Geuvers |primeiro1 =Herman |editor-sobrenome1 =Groote |editor-nome1 =Philippe de |título=The Curry–Howard isomorphism |publicado=Academia-Bruyland | series=Cahiers du Centre de logique (Université catholique de Louvain) | isbn=978-2-87209-363-2 | volume=8 |capítulo=The Calculus of Constructions and Higher Order Logic |páginas=139–191 |ano=1995}}, contains a synthetic introduction to the Curry–Howard correspondence.
* {{Citation |último1 =Gallier |primeiro1 =Jean H. |editor-sobrenome1 =Groote |editor-nome1 =Philippe de |título=The Curry–Howard isomorphism |publicado=Academia-Bruyland | series=Cahiers du Centre de logique (Université catholique de Louvain) | isbn=978-2-87209-363-2 | volume=8 |capítulo=On the Correspondence between Proofs and Lambda-Terms |capítulourl=ftp://ftp.cis.upenn.edu/pub/papers/gallier/cahiers.pdf |páginas=55–138 |ano=1995}}, contains a synthetic introduction to the Curry–Howard correspondence.

=== Livros ===
*{{Citation |editor-sobrenome1 =De Groote |editor-nome1 =Philippe |título=The Curry–Howard Isomorphism |publicado=Academia-Bruylant | series=Cahiers du Centre de Logique (Université catholique de Louvain) | isbn=978-2-87209-363-2 |ano=1995 | volume=8 |autor =edited by Ph. de Groote.}}, reproduces the seminal papers of Curry-Feys and Howard, a paper by de Bruijn and a few other papers.
* {{citation |último1 =Sørensen |primeiro1 =Morten Heine |último2 =Urzyczyn |primeiro2 =Paweł |título=Lectures on the Curry–Howard isomorphism |publicado=[[Elsevier Science]] |ano=2006 |anooriginal=1998 | isbn=978-0-444-52077-7 | volume=149 | series=Studies in Logic and the Foundations of Mathematics | url=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). ''[https://web.archive.org/web/20111002195146/http://www.monad.me.uk/stable/Proofs+Types.html 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). ''[http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ Type Theory and Functional Programming]'' Addison–Wesley. ISBN 0-201-41667-0.
* {{citation |último1 =Poernomo |primeiro1 =Iman |último2 =Crossley |primeiro2 =John |último3 =Wirsing |último4 =Martin |título=Adapting Proofs-as-Programs: The Curry–Howard Protocol |publicado=[[Springer Science+Business Media|Springer]] |ano=2005 |anooriginal=2005 | isbn=978-0-387-23759-6 | series=Monographs in Computer Science}}, 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.[http://www.site.uottawa.ca/~afelty/dist/gecco08.pdf]
* {{citation |último1 =de Queiroz |primeiro1 =Ruy J.G.B. |último2 =de Oliveira |primeiro2 =Anjolina G. |último3 =Gabbay |primeiro3 =Dov M. |  url=http://www.worldscibooks.com/compsci/8215.html |título=''The Functional Interpretation of Logical Deduction|publicado=[[Imperial College Press / World Scientific]] |ano=2011 |anooriginal=2011 | isbn=978-981-4360-95-1 | volume=5 | series=Advances in Logic }}.

== Leitura adicional ==
* [[P.T. Johnstone]], 2002, ''Sketches of an Elephant'', section D4.2 (vol 2) gives a [[categorical logic|categorical]] view of "what happens" in the Curry–Howard correspondence.

==Ligações externas==
{{Wikibooks|Haskell|The Curry–Howard isomorphism}}
*[https://web.archive.org/web/20080819185521/http://www.thenewsh.com/~newsham/formal/curryhoward/ The Curry–Howard Correspondence in Haskell]
*[http://www.haskell.org/wikiupload/1/14/TMR-Issue6.pdf The Monad Reader 6: Adventures in Classical-Land]: Curry–Howard in Haskell, Pierce's law.

{{DEFAULTSORT:Curry-Howard Correspondence}}
[[Categoria:Teoria dos tipos]]