Time and Location

  • Date: Friday, February 21
  • Time: 3:00-4:00 PM
  • Location: Luddy Hall 0119

Abstract

This talk explores the challenges of representing and manipulating variable bindings in formal verification and programming language theory, focusing on the formalization of the simply typed lambda calculus (STLC) in Lean using the locally nameless representation with cofinite quantification. This approach combines the readability of named representations with the automation-friendly properties of de Bruijn indices while simplifying the handling of bound variables, particularly in inductive proofs. We discuss the benefits of cofinite quantification, which enables strong induction principles. The talk covers the implementation of confluence and strong normalization proofs, highlighting the necessity of simultaneous and multivariable substitution. The talk is aimed at those interested in proof assistants, type theory, and automated reasoning, offering insights into the advantages and practical applications of this approach in Lean.