We use cookies to ensure that we give you the best experience on our website. By continuing to browse this repository, you give consent for essential cookies to be used. You can read more about our Privacy and Cookie Policy.

Durham Research Online
You are in:

An implementation of LF with coercive subtyping & universes.

Callaghan, P. and Luo, Z. (2001) 'An implementation of LF with coercive subtyping & universes.', Journal of automated reasoning., 27 (1). pp. 3-27.


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.

Item Type:Article
Additional Information:Special issue on Logical Frameworks.
Keywords:Type theory, Logical framework, Implementation.
Full text:Full text not available from this repository.
Publisher Web site:
Record Created:07 Oct 2008
Last Modified:10 Feb 2010 12:22

Social bookmarking: del.icio.usConnoteaBibSonomyCiteULikeFacebookTwitterExport: EndNote, Zotero | BibTex
Look up in GoogleScholar | Find in a UK Library