Polarisation in classical realisability and delimited control

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

• Guillaume Munch-Maccagnoni
• Tuesday 14 June 2011, 12:45-14:00
• Room SS03, Computer Laboratory, William Gates Building.

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

NOTE UNUSUAL TIME AND PLACE

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Room SS03, Computer Laboratory, William Gates Building
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.