![[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)
Guillaume Munch, Paris 7
Monday 17 May 2010, 12:45-14:00
A polarised calculus of delimited control
- đ¤ Speaker: Guillaume Munch, Paris 7
- đ Date & Time: Monday 17 May 2010, 12:45 - 14:00
- đ Venue: Room FW26, Computer Laboratory, William Gates Building
Abstract
Classical logic can be given a direct computational interpretation with control operators, but one might think there is no canonical interpretation as there are many control calculi, which is reflected by the number of double negation (or continuation-passing style) translations into intuitionistic logic.
Understanding what precisely can be encoded into lambda-calculus using continuation-passing style is made possible with the notion of polarity, as introduced by Girard in his 1992 article on classical logic.
After recalling all of the above, we extend the picture to delimited control operators, which allow continuations to be composed. By doing so we mean to give a calculus that accounts for existing delimited control calculi, as well as a polarised logic which decomposes type and effects systems.
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
- Interested Talks
- Martin's interesting talks
- Room FW26, Computer Laboratory, William Gates Building
- School of Technology
- Semantics Lunch (Computer Laboratory)
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.