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.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

Cited literature [25 references]  Display  Hide  Download

https://hal.inria.fr/inria-00295005
Contributor : Guillaume Munch-Maccagnoni <>
Submitted on : Friday, January 23, 2009 - 6:10:41 PM
Last modification on : Wednesday, January 23, 2019 - 10:29:22 AM
Long-term archiving on : Saturday, November 26, 2016 - 4:35:59 AM

File

etude_polarisee_du_systeme_l.p...
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00295005, version 4

Collections

Citation

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

Share

Metrics

Record views

570

Files downloads

124