カリー＝ハワード同型対応
この対応はCurry and Fays (1958)に於いて指摘された:最も単純なコンビネータ論理の一種におけるコンビネータ K と S が、驚くべきことにヒルベルト流の証明体系における公理図式 α → ( β → α ) {\displaystyle \alpha \to (\beta \to \alpha )} と ( α → ( β → γ ) ) → ( ( α → β ) → ( α → γ ) ) {\displaystyle (\alpha \to (\beta \to \gamma ))\to ((\alpha \to \beta )\to (\alpha \to \gamma ))} とにそれぞれ対応するのである。このことから、しばしば上記の公理図式はそれぞれ K と S と呼ばれる。ヒルベルト流の証明と見做せるプログラムの例が与えられる(後述)。
直観主義論理の含意断片に制限するならば、次のようにヒルベルト流の極めて簡明な形式化が存在する。いま Γ {\displaystyle \Gamma } を論理式の有限集合として、これを仮定と見做す。論理式 δ {\displaystyle \delta } が Γ {\displaystyle \Gamma } から導出可能である( Γ ⊢ δ {\displaystyle \Gamma \vdash \delta } )とは、以下の場合をいう:
δ {\displaystyle \delta } は仮定である、すなわち Γ {\displaystyle \Gamma } に属す、
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