Paper: Normalization and Extensionality (at LICS 1995)

Authors: Adolfo Piperno

Abstract

An investigation on the interaction between \beta-reduction and \eta-expansion is provided in a labelled \lambda-calculus, where additional information, that is constituted by integers, can be considered as a type in an abstract sense. This leads to propose the splitting of the $\beta$-rule into two parts: a restricted $\beta$-rule ($\bp$), strongly normalizing, and a reversed $\eta$-rule ($\etam$), which comes out to have different interpretations for reduction in untyped and typed calculi (static and dynamic allocation of computation resources, respectively). To substantiate the opportunity of this splitting, the paper provides new proofs of strong normalization theorems for some typed \lambda-calculi in Curry style (including the second order case) and discusses the applicability of the presented proof method to other type assignment systems.

BibTeX

  @InProceedings{Piperno-NormalizationandExt,
    author = 	 {Adolfo Piperno},
    title = 	 {Normalization and Extensionality},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS 1995)},
    year =	 {1995},
    month =	 {June}, 
    pages =      {300--310},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }