Lambda calculi based on substitution make variable binding hard to reason about and to mechanize. They also fail to capture common argument-passing paradigms such as named, positional, and optional arguments.

The authors define a core calculus that uses standard record types to model first-class environments and function arguments, with extensions supporting named, optional, and positional arguments and partial application. The calculus is then extended with mutable references, with stores also modelled as records. Everything is mechanized in Lean 4, using locally nameless representation for type variables. Derivation-depth-indexed relations serve as well-founded measures, and Lean's partial_fixpoint defines the interpreter.

Type soundness, normalization, a simulation of STLC, big-step equivalence, and syntax-directed typing are proved in about 29.6k lines of Lean across 1000 declarations. The development also includes an interpreter verified equivalent to the operational semantics.