Simply Typed Lambda Calculus
A project to formalize STLC with de Bruijn indices in Lean