Notes on the simply typed lambda calculus
Peter Aczel
In the Proceedings of the 1997 "Computational Logic" Advanced Study Institute International Summer School at Marktoberdorf, 1999. Original copy.
Abstracton and Computation, Chapter 1.3-1.4
Venanzio Capretta
PhD Thesis. Supervisor: Henk Barendregt. Defended on April 23, 2002. University of Nijmegen, The Netherlands. Original copy.