![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Focalisation and Classical Realisability
Focalisation and Classical RealisabilityAdd 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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsBiophysical Techniques Lecture Series 2017 Kettle's Yard ARTcrowd Theory WorkshopOther talksMandatory Madness: Colonial Psychiatry and British Mandate Palestine, 1920-48 UK 7T travelling-head study: pilot results Magnetic microscopy of meteorites: probing the magnetic state of the early solar system The Deciding Factor - An afternoon talk White dwarfs as tracers of cosmic, galactic, stellar & planetary evolution On Classical Tractability of Quantum Schur Sampling |