Abstract

In this talk, I extend and bring together distinct works of proof theory (term syntaxes for sequent calculus, focalisation and classical realisablity) and show their usefulness in practical applications to computer science.

After recalling the place of sequent calculus in computer science since the syntax of Curien-Herbelin (the lambda-bar-mu-mu-tilde calculus), I shall give a variant of this syntax which is suitable for sequent calculi that admit a focalising cut-elimination, such as Girard’s classical logic (LC) or linear logic (LL).

Focalisation makes the computational content of connectives more precise: it adds a distinction between strict (positive) and lazy (negative) connectives, thus expressing the order of evaluation in the types.

I then extend Krivine’s classical realisability to this setting and give examples of its applications. For instance, this tool allows us to quickly analyse the difference and the link between quantification and polymorphism à la ML in call-by-value, an issue related to the unsoundness of the first implementations of such polymorphism.

Guillaume is visiting Cambridge from April 29 to May 12.