Christian Urban
Mathematisches Institut der LMU

Nominal Techniques in Isabelle/HOL


In this talk, I will start with a brief motivation of the nominal logic work and then describe an inductive definition for alpha-equated lambda-terms. Building on that, I will illustrate how informal proofs about the lambda-calculus can be formalized with ease using strong induction principles that have Barendregt's variable convention already built-in.

Host:  Frank Pfenning
Appointments:  Jennifer Landefeld

Friday, November 11, 2005
2:00 p.m.
Wean Hall 7220

Principles of Programming Seminars