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 metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/inria-00409793
Contributor : Guillaume Munch-Maccagnoni <>
Submitted on : Tuesday, June 29, 2010 - 4:21:40 AM
Last modification on : Friday, January 4, 2019 - 5:33:25 PM
Long-term archiving on : Thursday, December 1, 2016 - 2:50:24 PM

File

focalisation_and_classical_rea...
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

408

Files downloads

231