カリー＝ハワード同型対応
もっと複雑な例として、 B {\displaystyle B} コンビネータに対応する定理を示そう。 B {\displaystyle B} の型は ( β → α ) → ( ( γ → β ) → ( γ → α ) ) {\displaystyle (\beta \to \alpha )\to ((\gamma \to \beta )\to (\gamma \to \alpha ))} である。 B {\displaystyle B} は S ( K S ) K {\displaystyle S(KS)K} に対応する(この事実は抽象除去などを用いて得られる)。これは目的の定理の証明の道筋を与えている。
まず K S {\displaystyle KS} を構成する。公理 K {\displaystyle K} の前にまず公理 S {\displaystyle S} の形を見る。そして公理 K {\displaystyle K} の α {\displaystyle \alpha } に公理 S {\displaystyle S} の論理式を代入する。すると次が得られる:
K : α → β → α {\displaystyle K:\alpha \to \beta \to \alpha }
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.