Etude polarisée du système L

Guillaume Munch-Maccagnoni 1, 2
1 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : Herbelin coined the name ``System L'' to refer to syntactical quotients of sequent calculi, in which two classes of terms interact in commands, in the manner of Curien's and Herbelin's lambda-bar-mu-mu-tilde calculus or Wadler's dual calculus. This paper introduces a system L that has constructs for all connectives of second order linear logic, and that shifts focus from the old code/environment interaction to a game between positives and negatives. L provides quotients for major second order sequent calculi, in their right-hand-side-sequents formulation as well as their two-sided-sequents formulation, namely LL, LK and LLP. The logician reader will appreciate the unifying framework for the study of sequent calculi it claims to be, whereas the computer scientist reader will appreciate the fact that it is a step toward Herbelin's project of rebuilding a theory of computation that puts ``call by name'' and ``call by value'' on an equal footing --- in particular is L involved with respect to reduction strategies, to wit that a cut elimination protocol that enjoys the Curch-Rosser property seems to stand out, and it allows to mix lazy and eager aspects. The principal tool for the study of this system is classical realizability, a consequence being that this tool is now extended to call by value.
Type de document :
Pré-publication, Document de travail
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger
Contributeur : Guillaume Munch-Maccagnoni <>
Soumis le : vendredi 23 janvier 2009 - 18:10:41
Dernière modification le : jeudi 10 mai 2018 - 01:32:32
Document(s) archivé(s) le : samedi 26 novembre 2016 - 04:35:59


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


  • HAL Id : inria-00295005, version 4



Guillaume Munch-Maccagnoni. Etude polarisée du système L. 2009. 〈inria-00295005v4〉



Consultations de la notice


Téléchargements de fichiers