Paul Callaghan, Zhaohui Luo. An Implementation of LF with Coercive Subtyping & Universes. Journal of Automated Reasoning, 27(1):3-27, 2001.
@article{CallaghanL01,
title = {An Implementation of LF with Coercive Subtyping & Universes},
author = {Paul Callaghan and Zhaohui Luo},
year = {2001},
tags = {subtyping},
researchr = {https://researchr.org/publication/CallaghanL01},
cites = {0},
citedby = {0},
journal = {Journal of Automated Reasoning},
volume = {27},
number = {1},
pages = {3-27},
}