カリー＝ハワード同型対応
⋆ ∘ t = ⋆ , {\displaystyle \star \circ t=\star ,}
π 1 ∘ ⟨ t , u ⟩ = t , π 2 ∘ ⟨ t , u ⟩ = u , ⟨ π 1 ∘ t , π 2 ∘ t ⟩ = t , {\displaystyle \pi _{1}\circ \langle t,u\rangle =t,\pi _{2}\circ \langle t,u\rangle =u,\langle \pi _{1}\circ t,\pi _{2}\circ t\rangle =t,}
e v a l ∘ ⟨ λ t , i d ⟩ = t , λ e v a l = i d . {\displaystyle eval\circ \langle \lambda t,id\rangle =t,\lambda eval=id.}
このとき、 t : α 1 × ... × α n ⟶ β {\displaystyle t:\alpha _{1}\times \ldots \times \alpha _{n}\longrightarrow \beta } なるモルフィズム t {\displaystyle t} が存在することと、 α 1 , ... , α n ⊢ β {\displaystyle \alpha _{1},\ldots ,\alpha _{n}\vdash \beta } なるシークエントが直観論理の含意論理積断片で証明可能であることとは同値である。上記のデカルト閉圏の射の等式体系として得られる計算模型はカテゴリカルコンビネータあるいは圏的コンビネータ論理として知られる。
ニコラース・ホーバート・ド・ブランはラムダ記法を証明検証器Automathにおいて用い、また命題をその証明の類として表現した。これはハワードが(CH対応に関する)原稿を書いた同時期の1960年後半のことであった。ド・ブランはハワードの仕事を知らず独立してこの対応を述べた(Sørensen & Urzyczyn [1998] 2006, pp 98–99)。一部の研究者は、カリー=ハワード対応という代りにカリー=ハワード=ド・ブラン対応という語を使用する。
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.)
K : ( ( α → β → γ ) → ( α → β ) → α → γ ) → δ → ( α → β → γ ) → ( α → β ) → α → γ {\displaystyle K:((\alpha \to \beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma )\to \delta \to (\alpha \to \beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma }
ここで S : ( α → β → γ ) → ( α → β ) → α → γ {\displaystyle S:(\alpha \to \beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma } とモーダス・ポネンスにより、
K S : δ → ( α → β → γ ) → ( α → β ) → α → γ {\displaystyle KS:\delta \to (\alpha \to \beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma }
次にこの論理式と公理 S {\displaystyle S} の最初の部分 α → β → γ {\displaystyle \alpha \to \beta \to \gamma } とが同一になるような代入を求め(ユニフィケーション)、
命題論理式に次のような構成規則を追加する場合を考える:
α {\displaystyle \alpha } が論理式で p {\displaystyle p} が命題変数ならば、 μ p . α {\displaystyle \mu p.\alpha } は論理式である。
この論理式の内容的な意味は循環的命題 [ t h i s / p ] α {\displaystyle [{\rm {this}}/p]\alpha } である。ただし [ μ q . β / p ] α {\displaystyle [\mu q.\beta /p]\alpha } なる論理式の内容的意味 [ [ t h i s / q ] β / p ] α {\displaystyle [[{\rm {this}}/q]\beta /p]\alpha } の中の this は命題全体ではなく [ t h i s / q ] β {\displaystyle [{\rm {this}}/q]\beta } を指示するものである。すなわち μ p . α {\displaystyle \mu p.\alpha } とは次の論理式の再帰方程式
X = [ X / p ] α {\displaystyle X=[X/p]\alpha }