- J. Lambek and P. J. Scott Introduction to Higher-Order Categorical Logic, Cambridge University Press, Cambridge Studies in Advanced Mathematics, no. 7, 1988
- William S. Hatcher ''[Review of] Peter Aczel. Frege Structures and the Notions of Proposition, Truth and Set. The Kleene Symposium, Proceedings of the Symposium Held June 18-24, 1978 at Madison, Wisconsin, U.S.A., edited by Jon Barwise, H. Jerome Keisler, Kenneth Kunen, Studies in Logic and the Foundations of Mathematics, vol. 101, North-Holland Publishing Company, Amsterdam, New York, and Oxford, 1980, pp. 31-59.,'' in: The Journal of Symbolic Logic, vol. 51, no. 1, 1986
- R. A. G. Seely ''Locally Cartesian Closed Categories and Type Theory,'' in: Mathematical Proceedings of the Cambridge Philosophical Society, vol. 95, no. 1, 1984
In his review of Peter Aczel's paper, William Hatcher writes, 'Both in the introduction and in the concluding section of the paper, Aczel says that the original stimulus to his work on Frege structures was an effort to build an appropriate lambda-calculus interpretation of Martin-Löf type theory. Robert Seely has recently established that models of Matin-Löf type theory are essentially the same thing as locally Cartesian closed categories […]. In the same vein, J. Lambek has established the equivalence of typed lambda calculus with Cartesian closed categories, and Dana Scott has shown that untyped lambda calculus is precisely the theory of a reflexive domain in a Cartesian closed category.' Thus the concept of Cartesian closed category is crucial importance to understanding Frege structures. So in order to learn Cartesian closed categories, I purchased the above textbook, Introduction to Higher-Order Categorical Logic.
