University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > A Heirarchy of Mendler style Iteration/Recursion Combinators: taming recursive types with negative occurrences

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity