An Implementation of LF with Coercive Subtyping & Universes

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},
}