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

https://hal.inria.fr/inria-00335718
Contributor : Julien Narboux <>
Submitted on : Thursday, October 30, 2008 - 12:40:34 PM
Last modification on : Thursday, April 23, 2020 - 2:26:30 PM
Long-term archiving on: : Tuesday, October 9, 2012 - 2:41:17 PM

File

SOS-lsfa08.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

358

Files downloads

972