カリー＝ハワード同型対応
De Bruijn, Nicolaas Govert (1995), “On the roles of types in mathematics”, in Groote, Philippe de, The Curry–Howard isomorphism, Cahiers du Centre de logique (Université catholique de Louvain), 8, Academia-Bruyland, pp. 27–54, ISBN 978-2-87209-363-2, http://alexandria.tue.nl/repository/freearticles/597627.pdf , the contribution of de Bruijn by himself.
Geuvers, Herman (1995), “The Calculus of Constructions and Higher Order Logic”, in Groote, Philippe de, The Curry–Howard isomorphism, Cahiers du Centre de logique (Université catholique de Louvain), 8, Academia-Bruyland, pp.
このとき、CL項 M {\displaystyle M} が Γ {\displaystyle \Gamma } のもとで型 δ {\displaystyle \delta } を持つ( Γ ⊢ M : δ {\displaystyle \Gamma \vdash M:\delta } )とは、以下の場合をいう:
M : δ {\displaystyle M:\delta } は Γ {\displaystyle \Gamma } に属す、
M : δ {\displaystyle M:\delta } は基本的なコンビネータの型付けである、すなわち: M : δ {\displaystyle M:\delta } は K : α → ( β → α ) {\displaystyle K:\alpha \to (\beta \to \alpha )} であるか、あるいは M : δ {\displaystyle M:\delta } は S : ( α → ( β → γ ) ) → ( ( α → β ) → ( α → γ ) ) {\displaystyle S:(\alpha \to (\beta \to \gamma ))\to ((\alpha \to \beta )\to (\alpha \to \gamma ))} である、
M : δ {\displaystyle M:\delta } は Γ ⊢ N : α → δ {\displaystyle \Gamma \vdash N:\alpha \to \delta } かつ R : α {\displaystyle R:\alpha } なるCL項 M {\displaystyle M} と N {\displaystyle N} の関数適用 ( N R ) {\displaystyle (NR)} である。
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. (September 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 .
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.