Document Open Access Logo

A Canonical Form for Universe Levels in Impredicative Type Theory

Author Yoan Géran

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.39.pdf
  • Filesize: 0.91 MB
  • 21 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Equational logic and rewriting
Keywords
  • universe levels
  • canonical form
  • impredicativity
  • imax algebra

Metrics

Abstract

The 0-imax-successor algebra, where imax: ℕ × ℕ → ℕ is the function defined by imax(n, 0) = 0 and imax(n, S(m)) = max(n, S(m)), is used to represent universe levels in impredicative type theory, in particular with universe polymorphism which introduces level variables, so it is present in proof systems such as Rocq and Lean. In particular, we need to know when two elements of this algebra are equivalent, and we may also want to decide the inequality. In this article, we introduce a canonical form for the terms of this algebra, and we provide a canonization algorithm. It permits deciding level equivalence by checking the canonical form equality, and also permits easily checking if a level is smaller than another one.

Cite As Get BibTex

Yoan Géran. A Canonical Form for Universe Levels in Impredicative Type Theory. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 39:1-39:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.39

Author Details

Yoan Géran
  • Mines Paris PSL, Centre de Recherche en Informatique, France
  • Université Paris-Saclay, Laboratoire Méthodes Formelles, ENS Paris-Saclay, France
  • Lab. ICube UMR 7357 CNRS Université de Strasbourg, France

Acknowledgements

I want to thank my PhD advisors Olivier Hermant and Gilles Dowek for the helpful discussions and comments.

Supplementary Materials

References

  1. Ali Assaf. A framework for defining computational higher-order logics. Theses, École polytechnique, September 2015. URL: https://pastel.archives-ouvertes.fr/tel-01235303.
  2. Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard. Dedukti : a Logical Framework based on the λΠ-Calculus Modulo Theory, 2016. Google Scholar
  3. Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, and Jiaxiang Liu. Encoding Proofs in Dedukti: the case of Coq proofs. In Proceedings Hammers for Type Theories, Proc. Higher-Order rewriting Workshop, Coimbra, Portugal, July 2016. Easy Chair. URL: https://inria.hal.science/hal-01330980.
  4. Henk Barendregt. Introduction to generalized type systems. Journal of Functional Programming, 1(2):125-154, 1991. URL: https://doi.org/10.1017/S0956796800020025.
  5. Henk Barendregt, S. Abramsky, D. Gabbay, T. Maibaum, and Henk (Hendrik) Barendregt. Lambda Calculi with Types, 2000. Google Scholar
  6. Stefano Berardi. Type dependence and Constructive mathematics. PhD thesis, PhD thesis, Dipartimento di Informatica, Torino, Italy, 1990. Google Scholar
  7. Frédéric Blanqui. Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:14, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.24.
  8. Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some Axioms for Mathematics. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), volume 195 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1-20:19, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.20.
  9. Mathieu Boespflug and Guillaume Burel. CoqInE: Translating the Calculus of Inductive Constructions into the λΠ-calculus Modulo. In "Second International Workshop on Proof Exchange for Theorem Proving, 2012. Google Scholar
  10. Mathieu Boespflug, Quentin Carbonneaux, and Olivier Hermant. The λΠ-calculus Modulo as a Universal Proof Language. CEUR Workshop Proceedings, 878, June 2012. URL: https://ceur-ws.org/Vol-878/paper2.pdf.
  11. Mario Carneiro. The Type Theory of Lean. Master’s thesis, Carnegie Mellon University, 2019. URL: https://github.com/digama0/lean-type-theory/releases.
  12. Thierry Coquand. An Analysis of Girard’s Paradox. In Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986), pages 227-236. IEEE Computer Society Press, June 1986. Google Scholar
  13. Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76(2):95-120, 1988. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  14. Judicaël Courant. Explicit Universes for the Calculus of Constructions. In Victor A. Carreño, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, pages 115-130, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-45685-6_9.
  15. Denis Cousineau and Gilles Dowek. Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo. In Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings, pages 102-117, June 2007. URL: https://doi.org/10.1007/978-3-540-73228-0_9.
  16. Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite Systems. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 243-320. Elsevier and MIT Press, 1990. URL: https://doi.org/10.1016/b978-0-444-88074-1.50011-1.
  17. Michael Färber. Safe, Fast, Concurrent Proof Checking for the Lambda-Pi Calculus modulo Rewriting. In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022, pages 225-238, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3497775.3503683.
  18. Gaspard Férey. Higher-Order Confluence and Universe Embedding in the Logical Framework. (Confluence d’ordre supérieur et encodage d’univers dans le Logical Framework). PhD thesis, École normale supérieure Paris-Saclay, France, 2021. URL: https://lmf.cnrs.fr/downloads/Perso/Ferey-thesis.pdf.
  19. Guillaume Genestier. Encoding Agda Programs Using Rewriting. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), volume 167 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:17, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.31.
  20. Girard, Jean-Yves. Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur, 1972. Google Scholar
  21. Yoan Géran. Mathématiques inversées de Coq. Master’s thesis, ENS Paris-Saclay, September 2021. URL: https://inria.hal.science/hal-04319183.
  22. Yoan Géran. STT∀ GeoCoq, 2021. URL: https://github.com/Karnaj/sttfa_geocoq_euclid.
  23. Robert Harper and Robert Pollack. Type Checking with Universes. In 2nd International Joint Conference on Theory and Practice of Software Development, TAPSOFT '89, pages 107-136, NLD, 1991. Elsevier Science Publishers B. V. URL: https://doi.org/10.1016/0304-3975(90)90108-T.
  24. Gabriel Hondet and Frédéric Blanqui. The New Rewriting Engine of Dedukti (System Description). In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), volume 167 of Leibniz International Proceedings in Informatics (LIPIcs), pages 35:1-35:16, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.35.
  25. Per Martin-Löf. A theory of types, 1971. Preprint, Stockholm University. Google Scholar
  26. Per Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. Studies in logic and the foundations of mathematics, 80:73-118, 1975. Google Scholar
  27. Per Martin-Löf. An intuitionistic theory of types. In Giovanni Sambin and Jan M. Smith, editors, Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, pages 127-172. Oxford University Press, 1998. Google Scholar
  28. Matthieu Sozeau and Nicolas Tabareau. Universe Polymorphism in Coq. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving, pages 499-514, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-08970-6_32.
  29. Terese. Term rewriting systems, volume 55 of Cambridge tracts in theoretical computer science. Cambridge University Press, 2003. Google Scholar
  30. François Thiré. Sharing a Library between Proof Assistants: Reaching out to the HOL Family. In Frédéric Blanqui and Giselle Reis, editors, Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018, volume 274 of EPTCS, pages 57-71, 2018. URL: https://doi.org/10.4204/EPTCS.274.5.
  31. Vladimir Voevodsky. A universe polymorphic type system, October 2014. An unfinished unreleased manuscript. URL: https://www.math.ias.edu/Voevodsky/files/files-annotated/Dropbox/Unfinished_papers/Type_systems/UPTS_current/Universe_polymorphic_type_sytem.pdf.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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