A Heirarchy of Mendler style Iteration/Recursion Combinators: taming recursive types with negative occurrences

Add to your list(s) Download to your calendar using vCal

• Ki Yung Ahn
• Monday 31 October 2011, 12:45-14:00
• FW26.

If you have a question about this talk, please contact Peter Sewell.

This talk is about the design of a small normalizing language Nax, named after Nax P. Mendler. In Nax, you are allowed to introduce arbitrary recursive types and eliminate them by principled iteration/recursion combinators following the style of Mendler’s. There are rich family of such combinators whose termination properties are well studied, where some of which are our own contribution (see our ICFP 2011 paper ).

The context of this work is to explore the design space of languages aiming for both (functional) programming and (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 but limit the formation recursive types. Our language Nax is an attempt to establish a core language having the good properties of the both worlds.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.