BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A polarised calculus of delimited control - Guillaume Munch\, Pari
 s 7
DTSTART:20100517T114500Z
DTEND:20100517T130000Z
UID:TALK24546@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:Classical logic can be given a direct computational interpreta
 tion with\ncontrol operators\, but one might think there is no canonical i
 nterpretation\nas there are many control calculi\, which is reflected by t
 he number of double\nnegation (or continuation-passing style) translations
  into intuitionistic\nlogic.\n\nUnderstanding what precisely can be encode
 d into lambda-calculus using continuation-passing\nstyle is made possible 
 with the notion of polarity\, as introduced by Girard\nin his 1992 article
  on classical logic.\n\nAfter recalling all of the above\, we extend the p
 icture to delimited control\noperators\, which allow continuations to be c
 omposed. By doing so we mean\nto give a calculus that accounts for existin
 g delimited control calculi\,\nas well as a polarised logic which decompos
 es type and effects systems.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR