An implementation of LF with coercive subtyping & universes

Abstract

We present Plastic, an implementation of LF with Coercive Subtyping, and focus on its implementation of Universes. LF is a variant of Martin-Löf''s logical framework, with explicitly typed -abstractions. We outline the system of LF with its extensions of inductive types and coercions. Plastic is the first implementation of this extended system; we discuss motivations and basic architecture and give examples of its use. LF is used to specify type theories. The theory UTT includes a hierarchy of universes that is specified in Tarski style. We outline the theory of these universes and explain how they are implemented in Plastic. Of particular interest is the relationship between universes and inductive types, and the relationship between universes and coercive subtyping. We 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.