Proof Automation and Metaprogramming in CSLib: Locally Nameless Lambda Calculi

Abstract: This talk will discuss CSLib's locally nameless formalization of lambda calculi, which currently includes STLC and System F with subtyping. While this is a well-established style of formalization, we use Lean's new proof automation features and metaprogramming in ways that are interesting to consider. We make heavy use of the grind tactic, allowing us to easily reuse existing Mathlib infrastructure for typing contexts and in general enable a succinct style that is approximately 45% fewer LoC than comparable formalizations. Metaprogramming has also been useful, allowing us to standardize certain notations and develop a single term elaborator for selecting fresh variables that does not require specialization for each type system.

logic in computer sciencemathematical softwareMathematics

Audience: researchers in the discipline

( slides | video )

Lean Together 2026