A polarised calculus of delimited control

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

• Guillaume Munch, Paris 7
• Monday 17 May 2010, 12:45-14:00
• Room FW26, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Sam Staton.

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.

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

This talk is included in these lists:

• All Talks (aka the CURE list)
• Computer Laboratory talks
• Room FW26, Computer Laboratory, William Gates Building
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.