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.
|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:||http://dx.doi.org/10.1023/A:1010648911114|
|Record Created:||07 Oct 2008|
|Last Modified:||10 Feb 2010 12:22|
|Social bookmarking:||Export: EndNote, Zotero | BibTex|
|Look up in GoogleScholar | Find in a UK Library|