Twelfth Annual IEEE Symposium on

Logic in Computer Science (LICS 1997)

Paper: Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets (at LICS 1997)

Authors: Roberto Di Cosmo Delia Kesner

Abstract

In this paper, we show the correspondence existing between normalization in calculi with explicit substitution and cut elimination in sequent calculus for Linear Logic, via Proof Nets. This correspondence allows us to prove that a typed version of the lambda-x-calculus is strongly normalizing, as well as of all the calculi that can be translated to it keeping normalization properties such as lambda-v, lambda-s, lambda-d, and lambda-f. In order to achieve this result, we introduce a new notion of reduction in Proof Nets: this extended reduction is still confluent and strongly normalizing, and is of interest of its own, as it corresponds to more identifications of proofs in Linear Logic that differ by inessential details. These results show that calculi with explicit substitutions are really an intermediate formalism between lambda calculus and proof nets, and suggest a completely new way to look at the problems still open in the field of explicit substitutions.

BibTeX

  @InProceedings{DiCosmoKesner-StrongNormalization,
    author = 	 {Roberto Di Cosmo and Delia Kesner},
    title = 	 {Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets},
    booktitle =  {Proceedings of the Twelfth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1997},
    year =	 1997,
    editor =	 {Glynn Winskel},
    month =	 {June}, 
    pages =      {35--46},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }