The Duality of Computation under Focus

Pierre-Louis Curien 1 Guillaume Munch-Maccagnoni 1
1 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 review the relationship between abstract machines for (call-by-name or call-by-value) λ-calculi (extended with Felleisen's $\mathcal C$) and sequent calculus, reintroducing on the way Curien-Herbelin's syntactic kit of the duality of computation. We provide a term language for a presentation of LK (with conjunction, disjunction, and negation), and we transcribe cut elimination as (non confluent) rewriting. A key slogan, which may appear here in print for the first time, is that commutative cut elimination rules are explicit substitution propagation rules. We then describe the focalised proof search discipline (in the classical setting), and narrow down the language and the rewriting rules to a confluent calculus (a variant of the second author's focalising system L). We then define a game of patterns and counterpatterns, leading us to a fully focalised finitary syntax for a synthetic presentation of classical logic, that provides a quotient on (focalised) proofs, abstracting out the order of decomposition of negative connectives.
Type de document :
Communication dans un congrès
Cristian S. Calude; Vladimiro Sassone. 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS) / Held as Part of World Computer Congress (WCC), Sep 2010, Brisbane, Australia. Springer, IFIP Advances in Information and Communication Technology, AICT-323, pp.165-181, 2010, Theoretical Computer Science. 〈10.1007/978-3-642-15240-5_13〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00491236
Contributeur : Hal Ifip <>
Soumis le : mercredi 6 août 2014 - 16:26:02
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : mercredi 26 novembre 2014 - 01:01:16

Fichier

03230167.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Pierre-Louis Curien, Guillaume Munch-Maccagnoni. The Duality of Computation under Focus. Cristian S. Calude; Vladimiro Sassone. 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS) / Held as Part of World Computer Congress (WCC), Sep 2010, Brisbane, Australia. Springer, IFIP Advances in Information and Communication Technology, AICT-323, pp.165-181, 2010, Theoretical Computer Science. 〈10.1007/978-3-642-15240-5_13〉. 〈inria-00491236v2〉

Partager

Métriques

Consultations de la notice

502

Téléchargements de fichiers

139