Скачать или смотреть Chris Henson - Locally Nameless Lambda Calculi (Lean Together 2026)

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.

---
Conference website: https://leanprover-community.github.i...
Full schedule: https://leanprover-community.github.i...
Lean community: https://leanprover-community.github.io/