We have previously published the Isabelle/HOL formalization of a general theory of syntax with bindings. In this 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.
This paper has been submitted to the Journal of Automated Reasoning. A draft of the paper is available here.
A zip archive with the Isabelle formalization is available here.
Lorenzo Gheri and Andrei Popescu