Skip to Main content Skip to Navigation
Conference papers

Focalisation and Classical Realisability (version with appendices)

Guillaume Munch-Maccagnoni 1, 2 
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Guillaume Munch-Maccagnoni Connect in order to contact the contributor
Submitted on : Tuesday, June 29, 2010 - 4:21:40 AM
Last modification on : Friday, January 21, 2022 - 3:21:25 AM
Long-term archiving on: : Thursday, December 1, 2016 - 2:50:24 PM


Files produced by the author(s)




Guillaume Munch-Maccagnoni. Focalisation and Classical Realisability (version with appendices). 18th EACSL Annual Conference on Computer Science Logic - CSL 09, Sep 2009, Coimbra, Portugal. pp.409-423, ⟨10.1007/978-3-642-04027-6_30⟩. ⟨inria-00409793v2⟩



Record views


Files downloads