Campus Event Calendar
Event Entry
What and Who
Nominal Techniques in the Theorem Prover Isabelle
Dr. Christian Urban
TU München
Talk
wttp://www4.in.tum.de/~urbanc/
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 14 December 2007
14:15
90 Minutes
E1 3 - Hörsaal Gebäude
528
Saarbrücken
Abstract
Dealing with binders, renaming of bound variables, capture-avoiding
substitution, etc., is very often a major problem in formal proofs,
especially in proofs by structural and rule induction. In two talks
I will describe a technique for formalising in Isabelle/HOL standard
"paper"-proofs about the lambda-calculus. For this I will present an
inductive definition for alpha-equated lambda-terms and strong
induction principles that have the variable convention already built
in. The aim of this work is to provide all proving technologies
necessary for reasoning conveniently about the lambda-calculus and
programming languages.
substitution, etc., is very often a major problem in formal proofs,
especially in proofs by structural and rule induction. In two talks
I will describe a technique for formalising in Isabelle/HOL standard
"paper"-proofs about the lambda-calculus. For this I will present an
inductive definition for alpha-equated lambda-terms and strong
induction principles that have the variable convention already built
in. The aim of this work is to provide all proving technologies
necessary for reasoning conveniently about the lambda-calculus and
programming languages.
Contact
Gerd Smolka
--email hidden
passcode not visible
logged in users only
Roxane Wetzel, 11/13/2007 08:59
Roxane Wetzel, 11/12/2007 15:25
Roxane Wetzel, 11/12/2007 15:23 -- Created document.
Roxane Wetzel, 11/12/2007 15:25
Roxane Wetzel, 11/12/2007 15:23 -- Created document.