coercive subtyping for the calculus of constructions
We present a coercive subtyping system for the calculus of constructions. The proposed system ? C CO over? 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 ? C CO over? and CC ? , this fact implies that ? C CO over? has confluence, subject reduction and strong normalization. We propose a formalization of coercion inference problem and present a sound and complete coercion inference algorithm.
subtyping calculus of constructions systems coercion extensibility case ident functional semantic interpretation sound completeness transitivity elimination transit reduction normalization formalism inference algorithm semantics of coercions conversation