Type Checking with Universes

Robert Harper, Robert Pollack. Type Checking with Universes. Theoretical Computer Science, 89(1):107-136, 1991.

Abstract

Abstract is missing.