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

A polarised calculus of delimited control



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.


Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

