Abstract

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)