Paper Info
Title
Formal SOS-Proofs for the Lambda-Calculus
Abstract
We 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.
Year
DOI
Venue
2009
10.1016/j.entcs.2009.07.053
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
nominal isabelle.,structural operational semantics,formal proof,lambda-calculus,proof assistants,actual theorem-prover code,definitional extention,paper formalisations,formal sos-proofs,great help,additional effort,usual big-step evaluation relation,theorem prover,nominal isabelle,lambda calculus,proof assistant
HOL,Discrete mathematics,Lambda calculus,Programming language,Computer science,Automated theorem proving,Mathematical proof,Semantics
Journal
Volume
ISSN
Citations 
247,
Electronic Notes in Theoretical Computer Science
2
PageRank 
References 
Authors
0.38
11
2
Name
Order
Citations
PageRank
Christian Urban114212.78
Julien Narboux213012.49