On the Church-Rosser property for expressive type systems and its consequences for their metatheoretic study
- 17 December 2002
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 320-329
- https://doi.org/10.1109/lics.1994.316057
Abstract
No abstract availableKeywords
This publication has 6 references indexed in Scilit:
- A new paradox in type theoryStudies in Logic and the Foundations of Mathematics, 1995
- Type Inference: Some Results, Some Problems1Fundamenta Informaticae, 1993
- A Complete Proof Synthesis Method for the Cube of Type SystemsJournal of Logic and Computation, 1993
- Modular proof of strong normalization for the calculus of constructionsJournal of Functional Programming, 1991
- "Type" is not a typePublished by Association for Computing Machinery (ACM) ,1986
- Constructions: A higher order proof system for mechanizing mathematicsPublished by Springer Nature ,1985