An implementation of LF with coercive subtyping and universes (Q5951521)

An implementation of a variant of Martin-Löf's logical framework with coercive subtyping, called LF, is presented. The paper begins with an outline of LF with its extensions of inductive types and coercions; then, motivations and the basic architecture of the implementation are given; finally, some examples are presented. In particular, special emphasis is put on the implementation of the the theory of a hierarchy of universes included in the object type theory UTT, which is outlined and implemented. The relationships between universes and inductive types, and between universes and coercive subtyping are studied and, as a conclusion, the authors claim that the combination of Tarski-style universes together with coercive subtyping provides an ideal formulation of universes that is both semantically clear and practical to use.