Document Open Access Logo

Subtype Universes

Authors Harry Maclean , Zhaohui Luo

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2020.9.pdf
  • Filesize: 0.75 MB
  • 16 pages

Document Identifiers

Author Details

Harry Maclean
  • Royal Holloway, University of London, UK
Zhaohui Luo
  • Royal Holloway, University of London, UK

Cite As Get BibTex

Harry Maclean and Zhaohui Luo. Subtype Universes. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.TYPES.2020.9

Abstract

We introduce a new concept called a subtype universe, which is a collection of subtypes of a particular type. Amongst other things, subtype universes can model bounded quantification without undecidability. Subtype universes have applications in programming, formalisation and natural language semantics. Our construction builds on coercive subtyping, a system of subtyping that preserves canonicity. We prove Strong Normalisation, Subject Reduction and Logical Consistency for our system via transfer from its parent system UTT[ℂ]. We discuss the interaction between subtype universes and other sorts of universe and compare our construction to previous work on Power types.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Type theory
  • coercive subtyping
  • subtype universe

Metrics

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

References

  1. David Aspinall. Subtyping with power types. In Computer Science Logic, 14th Annual Conference of the EACSL, Fischbachau, Germany, August 21-26, 2000 Proceedings, volume 1862 of Lecture Notes in Computer Science, pages 156-171. Springer, 2000. URL: https://doi.org/10.1007/3-540-44622-2_10.
  2. David Aspinall and Adriana B. Compagnoni. Subtyping dependent types (summary). In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 86-97. IEEE Computer Society, 1996. URL: https://doi.org/10.1109/LICS.1996.561307.
  3. Luca Cardelli. Structural subtyping and the notion of power type. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, USA, January 10-13, 1988, pages 70-79. ACM Press, 1988. URL: https://doi.org/10.1145/73560.73566.
  4. Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. An extension of system F with subtyping. Inf. Comput., 109(1-2):4-56, 1994. URL: https://doi.org/10.1006/inco.1994.1013.
  5. Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. ACM Comput. Surv., 17(4):471-522, 1985. URL: https://doi.org/10.1145/6041.6042.
  6. Giuseppe Castagna and Benjamin C. Pierce. Decidable bounded quantification. In Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, USA, January 17-21, 1994, pages 151-162. ACM Press, 1994. URL: https://doi.org/10.1145/174675.177844.
  7. Stergios Chatzikyriakidis and Zhaohui Luo. On the interpretation of common nouns: Types versus predicates. In Modern perspectives in type-theoretical semantics, pages 43-70. Springer, 2017. Google Scholar
  8. Thierry Coquand. An analysis of girard’s paradox. In Proceedings of the Symposium on Logic in Computer Science (LICS '86), Cambridge, Massachusetts, USA, June 16-18, 1986, pages 227-236. IEEE Computer Society, 1986. Google Scholar
  9. Jean-Yves Girard. Interprétation functionelle et Élimination des coupures dans l’arithmétique d’order supérieure. PhD thesis, Université Paris VII, 1972. Google Scholar
  10. Healfdene Goguen. The metatheory of UTT. In Types for Proofs and Programs, International Workshop TYPES'94, Båstad, Sweden, June 6-10, 1994, Selected Papers, volume 996 of Lecture Notes in Computer Science, pages 60-82. Springer, 1994. URL: https://doi.org/10.1007/3-540-60579-7_4.
  11. Zhaohui Luo. Computation and reasoning - a type theory for computer science, volume 11 of International series of monographs on computer science. Oxford University Press, 1994. Google Scholar
  12. Zhaohui Luo. Coercive subtyping. J. Log. Comput., 9(1):105-130, 1999. URL: https://doi.org/10.1093/logcom/9.1.105.
  13. Zhaohui Luo. Dependent record types revisited. In Proceedings of the 1st Workshop on Modules and Libraries for Proof Assistants, MLPA '09, page 30–37, New York, NY, USA, 2009. Association for Computing Machinery. URL: https://doi.org/10.1145/1735813.1735819.
  14. Zhaohui Luo. Formal semantics in modern type theories with coercive subtyping. Linguistics and Philosophy, 35(6):491-513, 2012. Google Scholar
  15. Zhaohui Luo, Sergei Soloviev, and Tao Xue. Coercive subtyping: Theory and implementation. Inf. Comput., 223:18-42, 2013. URL: https://doi.org/10.1016/j.ic.2012.10.020.
  16. Harry Maclean and Zhaohui Luo. Subtype universes (extended abstract). 26th International Conference on Types for Proofs and Programs (TYPES20), 2020. Google Scholar
  17. Per Martin-Löf. Intuitionistic type theory. Bibliopolis, 1984. Google Scholar
  18. Richard Montague. Formal Philosophy: Selected Papers of Richard Montague. Springer, 1974. Google Scholar
  19. Bengt Nordström, Kent Petersson, and Jan M Smith. Programming in Martin-Löf’s type theory. An introduction. Oxford University Press, 1990. Google Scholar
  20. Benjamin C. Pierce. Bounded quantification is undecidable. Inf. Comput., 112(1):131-165, 1994. URL: https://doi.org/10.1006/inco.1994.1055.
  21. Aarne Ranta. Type-Theoretical Grammar. Oxford University Press, 1994. Google Scholar
  22. John C. Reynolds. Towards a theory of type structure. In Programming Symposium, Proceedings Colloque sur la Programmation, Paris, France, April 9-11, 1974, volume 19 of Lecture Notes in Computer Science, pages 408-423. Springer, 1974. URL: https://doi.org/10.1007/3-540-06859-7_148.
  23. Sergei G. Vorobyov. Structural decidable extensions of bounded quantification. In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '95, page 164–175, New York, NY, USA, 1995. Association for Computing Machinery. URL: https://doi.org/10.1145/199448.199479.
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 About DROPS Imprint Privacy Contact