BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Heirarchy of Mendler style Iteration/Recursion Combinators: tami
 ng recursive types with negative occurrences - Ki Yung Ahn
DTSTART:20111031T124500Z
DTEND:20111031T140000Z
UID:TALK33917@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:This talk is about the design of a small normalizing language 
 Nax\, named after Nax P. Mendler. In Nax\, you are allowed to introduce ar
 bitrary recursive types and eliminate them by principled iteration/recursi
 on combinators following the style of Mendler's. There are rich family of 
 such combinators whose termination properties are well studied\, where som
 e of which are our own contribution (see our "ICFP 2011 paper":http://dx.d
 oi.org/10.1145/2034574.2034807 ).\n\nThe context of this work is to explor
 e the design space of languages aiming for both (functional) programming a
 nd (logical) reasoning. Most typed functional programming languages allow 
 formation of arbitrary recursive types with no guarantee of normalization.
  Many of the typed logical reasoning system are guaranteed to normalize bu
 t limit the formation recursive types. Our language Nax is an attempt to e
 stablish a core language having the good properties of the both worlds.
LOCATION:FW26
END:VEVENT
END:VCALENDAR