Title :
The Church-Rosser property for βη-reduction in typed λ-calculi
Author_Institution :
Fac. of Math. & Comput. Sci., Nijmegen Univ., Netherlands
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
Keywords :
data structures; formal logic; Church-Rosser property; beta eta -reduction; calculus of constructions; lambda calculus; pure type systems; typed lambda -calculi; Calculus; Chromium; Computer science; Lapping; Mathematics; Reactive power; Time of arrival estimation;
Conference_Titel :
Logic in Computer Science, 1992. LICS '92., Proceedings of the Seventh Annual IEEE Symposium on
Conference_Location :
Santa Cruz, CA
Print_ISBN :
0-8186-2735-2
DOI :
10.1109/LICS.1992.185556
