Document Open Access Logo

A Calculus of Constructions with Explicit Subtyping

Author Ali Assaf

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2014.27.pdf
  • Filesize: 0.54 MB
  • 20 pages

Document Identifiers

Author Details

Ali Assaf

Cite AsGet BibTex

Ali Assaf. A Calculus of Constructions with Explicit Subtyping. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 27-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.TYPES.2014.27

Abstract

The calculus of constructions can be extended with an infinite hierarchy of universes and cumulative subtyping. Subtyping is usually left implicit in the typing rules. We present an alternative version of the calculus of constructions where subtyping is explicit. We avoid problems related to coercions and dependent types by using the Tarski style of universes and by adding equations to reflect equality.
Keywords
  • type theory
  • calculus of constructions
  • universes
  • cumulativity
  • subtyping

Metrics

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

References

  1. Henk Barendregt. Lambda calculi with types. In Samson Abramsky, Dov M. Gabbay, and Thomas S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 117-309. Oxford University Press, 1992. Google Scholar
  2. Bruno Barras. Auto-validation d'un système de preuves avec familles inductives. PhD thesis, Université Paris 7, 1999. Google Scholar
  3. Bruno Barras and Benjamin Grégoire. On the role of type decorations in the calculus of inductive constructions. In Luke Ong, editor, Computer Science Logic, number 3634 in Lecture Notes in Computer Science, pages 151-166. Springer Berlin Heidelberg, 2005. Google Scholar
  4. Mathieu Boespflug and Guillaume Burel. CoqInE: Translating the calculus of inductive constructions into the λΠ-calculus modulo. In Proof Exchange for Theorem Proving-Second International Workshop, PxTP, page 44, 2012. Google Scholar
  5. Denis Cousineau and Gilles Dowek. Embedding pure type systems in the lambda-Pi-calculus modulo. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications, number 4583 in Lecture Notes in Computer Science, pages 102-117. Springer Berlin Heidelberg, 2007. Google Scholar
  6. Herman Geuvers and Freek Wiedijk. A logical framework with explicit conversions. Electronic Notes in Theoretical Computer Science, 199:33-47, February 2008. Google Scholar
  7. Robert Harper and Robert Pollack. Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions draft. In J. Díaz and F. Orejas, editors, TAPSOFT'89, number 352 in Lecture Notes in Computer Science, pages 241-256. Springer Berlin Heidelberg, 1989. Google Scholar
  8. Robert Harper and Robert Pollack. Type checking with universes. Theoretical Computer Science, 89(1):107-136, October 1991. Google Scholar
  9. Hugo Herbelin and Arnaud Spiwack. The Rooster and the Syntactic Bracket. In Ralph Matthes and Aleksy Schubert, editors, 19th International Conference on Types for Proofs and Programs (TYPES 2013), volume 26 of Leibniz International Proceedings in Informatics (LIPIcs), pages 169-187, Dagstuhl, Germany, 2014. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  10. Marc Lasson. Réalisabilité et paramétricité dans les systèmes de types purs. PhD thesis, Ecole normale supérieure de Lyon, 2012. Google Scholar
  11. Zhaohui Luo. CC^∞_ ⊂ and its meta theory. Laboratory for Foundations of Computer Science Report ECS-LFCS-88-58, 1988. Google Scholar
  12. Zhaohui Luo. ECC, an extended calculus of constructions. In Fourth Annual Symposium on Logic in Computer Science, 1989. LICS'89, Proceedings, pages 386-395, June 1989. Google Scholar
  13. Zhaohui Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, Inc., New York, NY, USA, 1994. Google Scholar
  14. Zhaohui Luo. Notes on universes in type theory. Lecture notes for a talk at Institute for Advanced Study, Princeton (http://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf), 2012.
  15. Per Martin-Löf and Giovanni Sambin. Intuitionistic type theory, volume 17. Bibliopolis Naples, 1984. Google Scholar
  16. Erik Palmgren. On universes in type theory. In Twenty-five years of constructive type theory, pages 191-204. Oxford University Press, October 1998. Google Scholar
  17. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  18. Ronan Saillard. Dedukti: a universal proof checker. In Foundation of Mathematics for Computer-Aided Formalization Workshop, 2013. Google Scholar
  19. Vincent Siles and Hugo Herbelin. Pure type system conversion is always typable. Journal of Functional Programming, 22(02):153-180, 2012. Google Scholar
  20. The Coq Development Team. The Coq Reference Manual, version 8.4, August 2012. Available electronically at URL: http://coq.inria.fr/doc.
  21. L. S. van Benthem Jutting, J. McKinna, and R. Pollack. Checking algorithms for pure type systems. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, number 806 in Lecture Notes in Computer Science, pages 19-61. Springer Berlin Heidelberg, 1994. Google Scholar
  22. Floris van Doorn, Herman Geuvers, and Freek Wiedijk. Explicit convertibility proofs in pure type systems. In Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP'13, pages 25-36, New York, NY, USA, 2013. ACM. Google Scholar
  23. Vincent van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, 1994. Google Scholar
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact