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.
Type de document :
Communication dans un congrès
Erich Grädel and Reinhard Kahle. 18th EACSL Annual Conference on Computer Science Logic - CSL 09, Sep 2009, Coimbra, Portugal. Springer-Verlag, 5771, pp.409-423, 2009, Lecture notes in computer science. 〈10.1007/978-3-642-04027-6_30〉
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00409793
Contributeur : Guillaume Munch-Maccagnoni <>
Soumis le : mardi 29 juin 2010 - 04:21:40
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : jeudi 1 décembre 2016 - 14:50:24

Fichier

focalisation_and_classical_rea...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

PPS | INRIA | USPC

Citation

Guillaume Munch-Maccagnoni. Focalisation and Classical Realisability (version with appendices). Erich Grädel and Reinhard Kahle. 18th EACSL Annual Conference on Computer Science Logic - CSL 09, Sep 2009, Coimbra, Portugal. Springer-Verlag, 5771, pp.409-423, 2009, Lecture notes in computer science. 〈10.1007/978-3-642-04027-6_30〉. 〈inria-00409793v2〉

Partager

Métriques

Consultations de la notice

382

Téléchargements de fichiers

163