Mathematisches Institut der LMU

Nominal
Techniques in Isabelle/HOL

Abstract:

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