Formal SOS-Proofs for the Lambda-Calculus

AbstractWe describe in this paper formalisations for the properties of weakening, type-substitutivity, subject-reduction and termination of the usual big-step evaluation relation. Our language is the lambda-calculus whose simplicity allows us to show actual theorem-prover code of the formal proofs. The formalisations are done in Nominal Isabelle, a definitional extention of the theorem prover Isabelle/HOL. The point of these formalisations is to be as close as possible to the “pencil-and-paper” proofs for these properties, but of course be completely rigorous. We describe where Nominal Isabelle is of great help with such formalisations and where one has to invest additional effort in order to obtain formal proofs