文章基本信息

标题：A Calculus of Constructions with Explicit Subtyping
本地全文：下载
作者：Ali Assaf
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：39
页码：27-46
DOI：10.4230/LIPIcs.TYPES.2014.27
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：The calculus of constructions can be extended with an infinite hierarchy of universes and cumulative subtyping. Subtyping is usually left implicit in the typing rules. We present an alternative version of the calculus of constructions where subtyping is explicit. We avoid problems related to coercions and dependent types by using the Tarski style of universes and by adding equations to reflect equality.
关键词：type theory; calculus of constructions; universes; cumulativity; subtyping