McKinna, J.; Pollack, R. Some Lambda Calculus and Type Theory Formalized. BRICS 1997, 4.