1 Search Results for "Xue, Tao"

Document
DOI: 10.4230/LIPIcs.TYPES.2013.251
Definitional Extension in Type Theory

Authors: Tao Xue

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

Abstract
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.
Cite as

Tao Xue. Definitional Extension in Type Theory. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 251-269, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{xue:LIPIcs.TYPES.2013.251,
  author =	{Xue, Tao},
  title =	{{Definitional Extension in Type Theory}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{251--269},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.251},
  URN =		{urn:nbn:de:0030-drops-46352},
  doi =		{10.4230/LIPIcs.TYPES.2013.251},
  annote =	{Keywords: conservative extension, definitional extension, subtype, coercive subtyping}
}
  • Refine by Author
  • 1 Xue, Tao

  • Refine by Classification

  • Refine by Keyword
  • 1 coercive subtyping
  • 1 conservative extension
  • 1 definitional extension
  • 1 subtype

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2014

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact