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 - 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
- Computer Laboratory talks
- Computing and Mathematics
- 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. |
## Other listsBiophysical Techniques Lecture Series 2017 Kettle's Yard ARTcrowd Theory Workshop## Other talksThe Partition of India and Migration White dwarfs as tracers of cosmic, galactic, stellar & planetary evolution The Deciding Factor - An afternoon talk Magnetic microscopy of meteorites: probing the magnetic state of the early solar system UK 7T travelling-head study: pilot results Mandatory Madness: Colonial Psychiatry and British Mandate Palestine, 1920-48 Black and British Migration Existence of Lefschetz fibrations on Stein/Weinstein domains Amino acid sensing: the elF2a signalling in the control of biological functions Protein Folding, Evolution and Interactions Symposium ***PLEASE NOTE THIS SEMINAR IS CANCELLED*** On Classical Tractability of Quantum Schur Sampling |