Skip to Main content Skip to Navigation
Conference papers

Formal SOS-Proofs for the Lambda-Calculus

Abstract : We describe in this paper formalisations for the properties of weakening, type-substitutivity, subject-reduction and termina- tion 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 de?nitional 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Julien Narboux Connect in order to contact the contributor
Submitted on : Thursday, October 30, 2008 - 12:40:34 PM
Last modification on : Thursday, January 6, 2022 - 11:38:04 AM
Long-term archiving on: : Tuesday, October 9, 2012 - 2:41:17 PM


Files produced by the author(s)




Christian Urban, Julien Narboux. Formal SOS-Proofs for the Lambda-Calculus. Third Workshop on Logical and Semantic Frameworks, with Applications, Mauricio Ayala-Rincón, Aug 2008, Salvador, Brazil. pp.139-155, ⟨10.1016/j.entcs.2009.07.053⟩. ⟨inria-00335718⟩



Record views


Files downloads