Robert Pollack: A Verified Typechecker. TLCA 1995: 365-380