BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Focalisation and Classical Realisability - Guillaume Munch\, Paris
  7
DTSTART:20090508T130000Z
DTEND:20090508T140000Z
UID:TALK18138@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:In this talk\, I extend and bring together distinct works of p
 roof theory (term syntaxes for sequent calculus\, focalisation and classic
 al\nrealisablity) and show their usefulness in practical applications to c
 omputer science.\n\nAfter recalling the place of sequent calculus in compu
 ter science since the syntax of Curien-Herbelin (the lambda-bar-mu-mu-tild
 e 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).\n\nFocalisation makes the comp
 utational content of connectives more precise: it adds a distinction betwe
 en strict (positive) and lazy (negative) connectives\, thus expressing the
  order of evaluation in the types.\n\nI then extend Krivine's classical re
 alisability to this setting and give examples of its applications. For ins
 tance\, this tool allows us to quickly analyse the difference and the link
  between quantification and polymorphism à la ML in call-by-value\, an is
 sue related to the unsoundness of the first implementations of such polymo
 rphism.\n\nGuillaume is visiting Cambridge from April 29 to May 12.
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR