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.

• Type: Conference
• Year: 2009
• Where: CSL
• Authors: Guillaume Munch-Maccagnoni
• Keywords: Artificial Intelligence, CSL 2009, Girard’s Classical Logic, Krivine’s Classical Realisability, Sequent Calculi