A Calculus of Constructions with Explicit Subtyping
Ali Assaf · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2015
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.