Conference paper
Focalisation and Classical Realisability
In Computer Science Logic (2009), volume 5771 of LNCS, pp. 409–423, Springer.
With appendices (PDF) (latest version: July 2009) — LaTeX macros
Abstract
We develop a polarised variant of Curien and Herbelin's lambda-bar-mu-mu-tilde calculus suitable for sequent calculi that admit a focalising cut elimination (i.e. whose proofs are focalised when cut-free), such as Girard's classical logic LC or linear logic. This gives a setting in which Krivine's classical realisability extends naturally (in particular to call-by-value), with a presentation in terms of orthogonality. We give examples of applications to the theory of programming languages.
In this version extended with appendices, we in particular give the two-sided formulation of LKpol with the involutive classical negation. We also show that there is in classical realisability a notion of internal completeness similar to the one of Ludics.
Talks
On the above paper:
- Focalization and Classical Realizability, GdT Sémantique et Réalisabilité, PPS, Paris.
- Focalisation and Classical Realisability, Logic and Semantics Seminar, Computer Lab, Cambridge.
- Classical Realisability and Focalisation, Réalisabilité à Chambéry Workshop, LAMA, Chambéry.
- Focalisation and Classical Realisability, CSL '09, Coimbra. (Slides)
