BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Structural recursion with pure local names - Andy Pitts (Universit
 y of Cambridge)
DTSTART:20091109T124500Z
DTEND:20091109T140000Z
UID:TALK20699@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:I will discuss a new recursion principle for inductive data mo
 dulo\nalpha-equivalence of bound names that makes use of Odersky-style\,\n
 effect-free local names when recursing over bound names. It is\ninspired b
 y the nominal sets notion of "alpha-structural\nrecursion". The new approa
 ch provides a pure calculus of total\nfunctions that still adequately repr
 esents alpha-structural recursion\nwhile avoiding the need to verify fresh
 ness side-conditions in\ndefinitions and computations. It arises from a ne
 w semantics of\nOdersky-style local names using nominal sets.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR