zbMATH — the first resource for mathematics

Aspects of higher order categorical logic. (English) Zbl 0549.03058
Mathematical applications of category theory, Proc. Spec. Sess. 89th Annu. Meet. Am. Math. Soc., Denver/Colo. 1983, Contemp. Math. 30, 145-174 (1984).
[For the entire collection see Zbl 0534.00008.]
This article surveys the authors’ work of recent years on the connections between \(\lambda\) -calculus and cartesian closed categories, and between higher-order type theory and toposes. It contains no results which cannot be found in the authors’ earlier papers (to which copious references are given); but it is pleasantly written, and makes an attractive trailer for their forthcoming book ”Introduction to higher order categorical logic” (Cambridge University Press, to appear).
Reviewer: P.T.Johnstone

03G30 Categorical logic, topoi
03B40 Combinatory logic and lambda calculus
18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.)
03B15 Higher-order logic; type theory (MSC2010)
18B25 Topoi