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} }