Coercive subtyping for the calculus of constructions

Abstract

We present a coercive subtyping system for the calculus of constructions. The proposed system λCCOover≤ is obtained essentially by adding coercions and η-conversion to λC≤[10], which is a subtyping extension to the calculus of constructions without coercions. Following [17, 18], the coercive subtyping c : A η B is understood as a special case of typing in arrow type c : A → B such that the term c behaves like an identity function. We prove that, with respect to this semantic interpretation, the proposed coercive subtyping system is sound and complete, and that this completeness leads to transitivity elimination (transitivity rule is admissible). In addition, we establish the equivalence between λCCOover≤ and CCßη, this fact implies that λCCOover≤ has confluence, subject reduction and strong normalization. We propose a formalization of coercion inference problem and present a sound and complete coercion inference algorithm.