Focalisation and Classical Realisability

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

• Guillaume Munch, Paris 7
• Friday 08 May 2009, 14:00-15:00
• Room FW11, Computer Laboratory, William Gates Building.

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.

This talk is included in these lists:

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

Note that ex-directory lists are not shown.