2026-08-17T16:44:22Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5490 2024-03-06T10:36:12Z ddc:004 open_access

A Calculus of Constructions with Explicit Subtyping Assaf, Ali type theory calculus of constructions universes cumulativity subtyping 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ali Assaf 2015 Is Part Of LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2014.27 urn:nbn:de:0030-drops-54904 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.27 eng https://creativecommons.org/licenses/by/3.0/legalcode