University of Cambridge > > Semantics Lunch (Computer Laboratory) > Polarisation in classical realisability and delimited control

Polarisation in classical realisability and delimited control

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

If you have a question about this talk, please contact Peter Sewell.


In the quest of a proofs-as-programs interpretation of real-world mathematics, surely the big scale is interesting (for instance axioms with involved computational content such as dependent choice) but the small scale is equally important (operational details inspired by CPS and linear logic semantics, such as polarities).

One striking polarity-related phenomenon is the duality between the call-by-value and the call-by-name evaluation paradigms in the presence of call/cc-like control operators. Curien and Herbelin (2000) captured this phenomenon in an elegant way with a symmetric syntax that could express the symmetries of sequent calculus. I will argue that this result is more than a beautiful curiosity—- it also provides us with a new tool for investigating the proofs-as-programs correspondence in a unified fashion.

First I would like to explain the path from lambda calculus to Girard’s polarised classical logic using stepping stones from the semantics of programming languages (Moggi’s monadic calculus, duality between call-by-name and call-by-value, call-by-push-value).

Then I would like to sketch in a nutshell how a polarised variant of Curien-Herbelin’s notation can help to show

  • the importance of phenomena linked to polarisation in Krivine’s classical realisability, and
  • how polarisation can help answer the question “what is a call-by-name counterpart to Danvy-Filinski’s delimited control calculus?”. (Confirming results from my last year’s work-in-progress talk)

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-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity