Sciweavers

CSL
2009
Springer

Focalisation and Classical Realisability

13 years 10 months ago
Focalisation and Classical Realisability
We develop a polarised variant of Curien and Herbelin’s ¯λµ˜µ 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.
Guillaume Munch-Maccagnoni
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where CSL
Authors Guillaume Munch-Maccagnoni
Comments (0)