2026-06-06T10:25:06Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4635 2024-03-06T10:35:10Z ddc:004 open_access

Definitional Extension in Type Theory Xue, Tao conservative extension definitional extension subtype coercive subtyping When we extend a type system, the relation between the original system and its extension is an important issue we want to know. Conservative extension is a traditional relation we study with. But in some cases, like coercive subtyping, it is not strong enough to capture all the properties, more powerful relation between the systems is required. We bring the idea definitional extension from mathematical logic into type theory. In this paper, we study the notion of definitional extension for type theories and explicate its use, both informally and formally, in the context of coercive subtyping. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Tao Xue 2014 Is Part Of LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2013.251 urn:nbn:de:0030-drops-46352 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.251 eng https://creativecommons.org/licenses/by/3.0/legalcode