Document Open Access Logo

Definitional Extension in Type Theory

Author Tao Xue

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2013.251.pdf
  • Filesize: 0.53 MB
  • 19 pages

Document Identifiers

Author Details

Tao Xue

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.TYPES.2013.251

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.
Keywords
  • conservative extension
  • definitional extension
  • subtype
  • coercive subtyping

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. David Aspinall and Adriana Compagnoni. Subtyping dependent types. Theoretical Computer Science, 266(1-2):273-309, 2001. Google Scholar
  2. Gilles Barthe and Maria João Frade. Constructor subtyping. In S. Doaitse Swierstra, editor, Proceedings of Programming Languages and Systems, 8 conf. (ESOP'99), volume 1576 of Lecture Notes in Computer Science, pages 109-127. Springer, 1999. Google Scholar
  3. Robert Harper, Furio Honsell, and Gordon D. Plotkin. A framework for defining logics. In Proceedings of Symposium on Logic in Computer Science 1987, pages 194-204. IEEE Computer Society, 1987. Google Scholar
  4. Martin Hofmann. Extensional Concepts in Intensional Type Theory. PhD thesis, University of Edinburgh, 1995. Google Scholar
  5. Stephen Kleene. Introduction to Metamathematics. North Holland, 1952. Google Scholar
  6. Zhaohui Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, 1994. Google Scholar
  7. Zhaohui Luo. Coercive subtyping. Journal of Logic and Computation, 9(1):105-130, 1999. Google Scholar
  8. Zhaohui Luo. D-conservativity. Notes, January 2012. Google Scholar
  9. Zhaohui Luo. Formal semantics in modern type theories with coercive subtyping. Linguistics and Philosophye, 35(6):491-513, 2012. Google Scholar
  10. Zhaohui Luo and Robert Pollack. Lego proof development system: User manual, 1992. Google Scholar
  11. Zhaohui Luo, Sergei Soloviev, and Tao Xue. Coercive subtyping: Theory and implementation. Information and Computation, 223:18-42, February 2013. Google Scholar
  12. Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Google Scholar
  13. Robin Milner. A theory of type polymorphism in programming. Journal of Computer Systems and Sciences, 17:348-375, 1978. Google Scholar
  14. John C. Mitchell. Type inference with simple subtypes. Journal of Functional Programming, 1(3):245-285, 1991. Google Scholar
  15. Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf’s Type Theory: An Introduction. Oxford University Press, Oxford, 1990. Google Scholar
  16. Robert Pollack. Implicit syntax. In the preliminary Proceedings of the 1st Workshop on Logical Frameworks, 1990. Google Scholar
  17. Sergei Soloviev and Zhaohui Luo. Coercion completion and conservativity in coercive subtyping. Annals of Pure and Applied Logic, 113(1-3):297-322, 2002. Google Scholar
  18. Tao Xue. Theory and Implementation of Coercive Subtyping. PhD thesis, Royal Holloway, University of London, 2013. Google Scholar
  19. Tao Xue and Zhaohui Luo. Dot-types and their implementaion. Logical Aspects of Computational Linguistics (LACL'12). LNCS, 7351:234-249, 2012. Google Scholar
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