Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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 metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Guillaume Munch-Maccagnoni Connect in order to contact the contributor
Submitted on : Friday, January 23, 2009 - 6:10:41 PM
Last modification on : Sunday, June 26, 2022 - 11:49:19 AM
Long-term archiving on: : Saturday, November 26, 2016 - 4:35:59 AM


Files produced by the author(s)


  • HAL Id : inria-00295005, version 4



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



Record views


Files downloads