Document Open Access Logo

Cumulative Inductive Types In Coq

Authors Amin Timany, Matthieu Sozeau

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2018.29.pdf
  • Filesize: 0.62 MB
  • 16 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Lambda calculus
Keywords
  • Coq
  • Proof Assistants
  • Inductive Types
  • Universes
  • Cumulativity

Metrics

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

Abstract

In order to avoid well-known paradoxes associated with self-referential definitions, higher-order dependent type theories stratify the theory using a countably infinite hierarchy of universes (also known as sorts), Type_0 : Type_1 : *s. Such type systems are called cumulative if for any type A we have that A : Type_i implies A : Type_{i+1}. The Predicative Calculus of Inductive Constructions (pCIC) which forms the basis of the Coq proof assistant, is one such system. In this paper we present the Predicative Calculus of Cumulative Inductive Constructions (pCuIC) which extends the cumulativity relation to inductive types. We discuss cumulative inductive types as present in Coq 8.7 and their application to formalization and definitional translations.

Cite As Get BibTex

Amin Timany and Matthieu Sozeau. Cumulative Inductive Types In Coq. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSCD.2018.29

Author Details

Amin Timany
  • imec-Distrinet, KU Leuven, Leuven, Belgium
Matthieu Sozeau
  • Inria Paris & IRIF, Paris, France

References

  1. Peter Aczel. An Introduction to Inductive Definitions. Studies in Logic and the Foundations of Mathematics, 90:739-782, 1977. Google Scholar
  2. Peter Aczel. On Relating Type Theories and Set Theories. In Thorsten Altenkirch, Bernhard Reus, and Wolfgang Naraschewski, editors, TYPES'98, pages 1-18. Springer Berlin Heidelberg, 1999. Google Scholar
  3. Bruno Barras. Semantical Investigation in Intuitionistic Set Theory and Type Theoris with Inductive Families, 2012. Habilitation thesis draft, University Paris Diderot - Paris 7. Google Scholar
  4. Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau. The Next 700 Syntactical Models of Type Theory. In CPP 2017, pages 182-194, Paris, France, 2017. URL: http://dx.doi.org/10.1145/3018610.3018620.
  5. Frank R Drake. Set theory : an introduction to large cardinals. Studies in logic and the foundations of mathematics 76. North-Holland, Amsterdam, 1974. Google Scholar
  6. Peter Dybjer. Inductive Sets and Families in Martin-Löf’s Type Theory and Their Set-Theoretic Semantics, pages 280-306. Cambridge University Press, Cambridge, 1991. Google Scholar
  7. Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris VII, 1972. Google Scholar
  8. 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, pages 241-256, Berlin, Heidelberg, 1989. Springer Berlin Heidelberg. Google Scholar
  9. Antonius JC Hurkens. A simplification of Girard’s paradox. In International Conference on Typed Lambda Calculi and Applications, pages 266-278, Edinburgh, UK, 1995. Springer. Google Scholar
  10. Gyesik Lee and Benjamin Werner. Proof-irrelevant model of CC with predicative induction and judgmental equality. Logical Methods in Computer Science, 7(4), 2011. URL: http://dx.doi.org/10.2168/LMCS-7(4:5)2011.
  11. Conor McBride. Universe hierarchies, 2015. Blog post. Google Scholar
  12. C. Paulin-Mohring. Définitions Inductives en Théorie des Types d'Ordre Supérieur. Habilitation à diriger les recherches, Université Claude Bernard Lyon I, 1996. Google Scholar
  13. Damien Rouhling. Dependently typed lambda calculus with a lifting operator. Technical report, ENS Lyon, May-August 2014. Internship report. Google Scholar
  14. Vincent Siles and Hugo Herbelin. Pure type system conversion is always typable. J. Funct. Program., 22(2):153-180, 2012. URL: http://dx.doi.org/10.1017/S0956796812000044.
  15. Matthieu Sozeau and Nicolas Tabareau. Universe Polymorphism in Coq. In Interactive Theorem Proving 2014, pages 499-514, Vienna, Austria, 2014. Springer. URL: http://dx.doi.org/10.1007/978-3-319-08970-6_32.
  16. The Coq Development Team. The Coq Proof Assistant, version 8.7.1, dec 2017. URL: http://dx.doi.org/10.5281/zenodo.1133970.
  17. Amin Timany and Bart Jacobs. First Steps Towards Cumulative Inductive Types in CIC. In Theoretical Aspects of Computing, pages 608-617, Cali, Colombia, 2015. Springer. URL: http://dx.doi.org/10.1007/978-3-319-25150-9_36.
  18. Amin Timany and Bart Jacobs. Category Theory in Coq 8.5. In Formal Structures for Computation and Deduction, pages 30:1-30:18, Porto, Portugal, 2016. LIPIcs. URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.30.
  19. Amin Timany and Matthieu Sozeau. Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC). Research Report 9105, KU Leuven ; Inria Paris, 2017. URL: https://hal.inria.fr/hal-01615123.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact