Dependent Coercions
Zhaohui Luo, Sergei Soloviev · Electronic Notes in Theoretical Computer Science · 1999
A notion of dependent coercion is introduced and studied in the context of dependent type theories. It extends our earlier work on coercive subtyping into a uniform framework which increases the expressive power with new applications. A dependent coercion introduces a subtyping relation between a type and a family of types in that an object of the type is mapped into one of the types in the family. We present the formal framework, discuss its meta-theory, and consider applications such as its use in functional programming with dependent types.