McKinna, J. and Pollack, R. 1997. Some Lambda Calculus and Type Theory Formalized. BRICS Report Series. 4, 51 (Jun. 1997). DOI:https://doi.org/10.7146/brics.v4i51.19272.