An Implementation of LF with Coercive Subtyping & Universes Export

@article{citeulike:6059696, 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\"{o}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.}, author = {Callaghan, Paul and Luo, Zhaohui}, citeulike-article-id = {6059696}, citeulike-linkout-0 = {http://dx.doi.org/10.1023/A:1010648911114}, citeulike-linkout-1 = {http://www.springerlink.com/content/u5402x2m45451t47}, day = {1}, doi = {10.1023/A:1010648911114}, journal = {Journal of Automated Reasoning}, keywords = {dependent-types, universe}, month = {July}, number = {1}, pages = {3--27}, posted-at = {2009-11-03 10:39:12}, priority = {2}, title = {An Implementation of LF with Coercive Subtyping \& Universes}, url = {http://dx.doi.org/10.1023/A:1010648911114}, volume = {27}, year = {2001} }

TY - JOUR ID - citeulike:6059696 L3 - citeulike-article-id:6059696 N2 - 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. IS - 1 JF - Journal of Automated Reasoning EP - 27 TI - An Implementation of LF with Coercive Subtyping & Universes VL - 27 SP - 3 KW - dependent-types KW - universe AU - Callaghan, Paul AU - Luo, Zhaohui PY - 2001/07/01/ UR - http://dx.doi.org/10.1023/A:1010648911114 ER -