Robert Harper, Robert Pollack. Type Checking with Universes. Theoretical Computer Science, 89(1):107-136, 1991.
@article{HarperP91,
title = {Type Checking with Universes},
author = {Robert Harper and Robert Pollack},
year = {1991},
tags = {type checking},
researchr = {https://researchr.org/publication/HarperP91},
cites = {0},
citedby = {0},
journal = {Theoretical Computer Science},
volume = {89},
number = {1},
pages = {107-136},
}