Logic in Computer Science (LICS 1992)

Paper: The Church-Rosser property for βη-reduction in typed λ-calculi (at LICS 1992)

Authors: Geuvers, H.

Abstract

The Church-Rosser property (CR) for pure type systems with βη-reduction is investigated. It is proved that CR (for βη) on the well-typed terms of a fixed type holds, which is the maximum one can expect in view of Nederpelt's (1973) counterexample. The proof is given for a large class of pure type systems that contains, e.g., LF F, Fω, and the calculus of constructions

BibTeX

  @InProceedings{Geuvers-TheChurchRosserprop,
    author = 	 {Geuvers, H.},
    title = 	 {The Church-Rosser property for βη-reduction in typed λ-calculi },
    booktitle =  {Proceedings of the Seventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1992},
    year =	 1992,
    editor =	 {Andre Scedrov},
    month =	 {June}, 
    pages =      {453--460},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }