Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS

TL;DR

This paper formalizes key properties of lambda-calculus, including semantics, Church-Rosser, and standardization theorems, using Isabelle/HOL, covering both call-by-name and call-by-value variants with higher-order abstract syntax encoding.

Contribution

It applies a general formal theory to lambda-calculus, enabling rigorous proofs of fundamental properties and extending prior work with detailed formalization.

Findings

Formalization of semantics, Church-Rosser, and standardization theorems

Coverage of call-by-name and call-by-value lambda-calculus

Use of general theory to streamline proofs and reasoning

Abstract

We have previously published the Isabelle/HOL formalization of a general theory of syntax with bindings. In this companion paper, we instantiate the general theory to the syntax of lambda-calculus and formalize the development leading to several fundamental constructions and results: sound semantic interpretation, the Church-Rosser and standardization theorems, and higher-order abstract syntax (HOAS) encoding. For Church-Rosser and standardization, our work covers both the call-by-name and call-by-value versions of the calculus, following classic papers by Takahashi and Plotkin. During the formalization, we were able to stay focused on the high-level ideas of the development -- thanks to the arsenal provided by our general theory: a wealth of basic facts about the substitution, swapping and freshness operators, as well as recursive-definition and reasoning principles, including a specialization to semantic interpretation of syntax.