An implementation of LF with coercive subtyping & universes

Callaghan, P.; Luo, Zhaohui

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.

Citation

Callaghan, P., & Luo, Z. (2001). An implementation of LF with coercive subtyping & universes. Journal of Automated Reasoning, 27(1), 3-27. https://doi.org/10.1023/a%3A1010648911114

• Journal Article Type: Article
• Publication Date: 2001-07
• Deposit Date: Oct 7, 2008
• Journal: Journal of Automated Reasoning
• Print ISSN: 0168-7433
• Electronic ISSN: 1573-0670
• Publisher: Springer
• Peer Reviewed: Peer Reviewed
• Volume: 27
• Issue: 1
• Pages: 3-27
• DOI: https://doi.org/10.1023/a%3A1010648911114
• Keywords: Type theory, Logical framework, Implementation.
• Public URL: https://durham-repository.worktribe.com/output/1627959
• Publisher URL: http://www.springerlink.com/content/u5402x2m45451t47/?p=207a4f6c528240b5a076c9f7c56db6ae&pi=1