BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A New Version of Nominal Isabelle - Christian Urban (TUM)
DTSTART:20100216T130000Z
DTEND:20100216T140000Z
UID:TALK22758@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Nominal Isabelle is a definitional extension of Isabelle/HOL f
 or reasoning conveniently about languages involving binders. In this talk\
 , I will describe a new formalisation of the most basic concepts in the no
 minal logic work. This new formalisation is a much better fit with the rea
 soning infrastructure provided by Isabelle/HOL. A result is that we can ma
 ke Nominal Isabelle\neasier to use and can also reduce drastically the amo
 unt of\ncustom ML-code in our implementation of Nominal Isabelle.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR