Coherence is a vital requirement for the correct use of coercive subtyping for abbreviation and other applications. However, some coercions are incoherent, although very useful. A typical example of such is the subtyping rules for ∑-types: the component-wise rules and the rule of the first projection. Both of these groups of rules are often used in practice (and coherent themselves), but they are incoherent when put together directly. In this paper, we study this case for ∑-types by introducing a new subtyping relation and the resulting system enjoys the properties of coherence and admissibility of substitution and transitivity. © Springer-Verlag 2004.
CITATION STYLE
Luo, Y., & Luo, Z. (2004). Combining Incoherent Coercions for ∑-Types. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3085, 276–292. https://doi.org/10.1007/978-3-540-24849-1_18
Mendeley helps you to discover research relevant for your work.