The Church-Rosser property for beta eta -reduction in typed lambda -calculi
- 2 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 453-460
- https://doi.org/10.1109/lics.1992.185556
Abstract
The Church-Rosser property (CR) for pure type systems with beta eta -reduction is investigated. It is proved that CR (for beta eta ) 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 omega , and the calculus of constructions.Keywords
This publication has 3 references indexed in Scilit:
- Unification and anti-unification in the calculus of constructionsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A framework for defining logicsJournal of the ACM, 1993
- Modular proof of strong normalization for the calculus of constructionsJournal of Functional Programming, 1991