University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > A polarised calculus of delimited control

A polarised calculus of delimited control

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

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.

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