![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Monday 31 October 2011, 12:45-14:00
A Heirarchy of Mendler style Iteration/Recursion Combinators: taming recursive types with negative occurrences
- đ¤ Speaker: Ki Yung Ahn
- đ Date & Time: Monday 31 October 2011, 12:45 - 14:00
- đ Venue: FW26
Abstract
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.
Series This talk is part of the Semantics Lunch (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Department of Computer Science and Technology talks and seminars
- FW26
- Interested Talks
- Martin's interesting talks
- School of Technology
- Semantics Lunch (Computer Laboratory)
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.