Paper: Normalisation is insensible to lambda-term identity or difference (at LICS 2006)

Authors: Mariangiola Dezani-Ciancaglini Makoto Tatsuta

Abstract

This paper analyses the computational behaviour of ë- term applications. The properties we are interested in are weak normalisation (i.e. there is a terminating reduction) and strong normalisation (i.e. all reductions are terminating).

BibTeX

  @InProceedings{DezaniCiancagliniTa-Normalisationisinse,
    author = 	 {Mariangiola Dezani-Ciancaglini and Makoto Tatsuta},
    title = 	 {Normalisation is insensible to lambda-term identity or difference},
    booktitle =  {Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science (LICS 2006)},
    year =	 {2006},
    month =	 {August}, 
    pages =      {327--336},
    location =   {Seattle, Washington, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }