The representation and manipulation of variable bindings present significant challenges in formal verification and programming language theory. This talk delves into these challenges by exploring the formalization of locally nameless syntax with cofinite quantification within the simply typed lambda calculus (STLC) using the Lean proof assistant*.

Our primary objective is to formalize STLC in Lean, using the locally nameless representation combined with cofinite quantification, namely, a cofinite style of quantification for introducing free names in rules dealing with binders*. This approach is chosen for its significant advantages in simplifying proofs and enhancing the robustness of formal systems. The locally nameless representation balances the ease of automated reasoning provided by de Bruijn indices with the human-readability of named representations. Cofinite quantification further simplifies the handling of bound variables, particularly in inductive proofs and recursive functions. Cofinite quantification also enables strong induction principles, which have been effectively used to formalize various type systems and semantics.

In this talk, we will introduce the locally nameless representation* and its benefits over traditional methods, and discuss the concept and implementation of cofinite quantification. We will also cover practical applications in the formal verification of STLC in Lean, highlighting the proof and formalization of confluence and strong normalization. Our approach proposes simultaneous and multivariable substitution as necessary steps to prove the normalization theorem. The choice of Lean4 for formalizing the theory will be justified with its specific advantages.

The significance of this work lies in its novelty: to the best of our knowledge, this is the first formalization of STLC in locally nameless syntax that includes both confluence and strong normalization. This pioneering effort sets a new standard for the formal verification of programming languages, demonstrating the practical viability and benefits of this approach. Moreover, we have achieved a complete formalization of all results we achieved in Lean, ensuring that our findings are verifiable and reproducible within the proof assistant framework.

This talk is intended for anyone interested in automated proofs, the formalization of mathematics, proof assistants, and type theory. Attendees will gain insights into the practical implementation of locally nameless syntax and cofinite quantification in Lean, along with their theoretical underpinnings and advantages. Through the case study, we will illustrate how this approach can simplify the formalization process and improve the reliability of proofs.

*References are included in the abstract file.