Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions (Draft)

Robert Harper, Robert Pollack. Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions (Draft). In Josep Díaz, Fernando Orejas, editors, TAPSOFT 89: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Barcelona, Spain, March 13-17, 1989, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Is. Volume 352 of Lecture Notes in Computer Science, pages 241-256, Springer, 1989.

Abstract

Abstract is missing.