University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Focalisation and Classical Realisability

Focalisation and Classical Realisability

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

If you have a question about this talk, please contact Sam Staton.

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.

This talk is part of the Logic and Semantics Seminar (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-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity