Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus by Michael Rawson 📧 Jul 09