Document Open Access Logo

Definitional Proof Irrelevance Made Accessible

Authors Thiago Felicissimo , Yann Leray , Loïc Pujet , Nicolas Tabareau , Éric Tanter , Théo Winterhalter

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.41.pdf
  • Filesize: 1.01 MB
  • 26 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Dependent type theory
  • proof assistants
  • Rocq
  • proof irrelevance
  • accessibility predicates
  • observational equality
  • canonicity
  • set-theoretic models

Metrics

Abstract

A universe of propositions equipped with definitional proof irrelevance constitutes a convenient medium to express properties and proofs in type-theoretic proof assistants such as Lean, Rocq, and Agda. However, allowing accessibility predicates - used to establish semantic termination arguments - to inhabit such a universe yields undecidable typechecking, hampering the predictability and foundational bases of a proof assistant. To effectively reconcile definitional proof irrelevance and accessibility predicates with both theoretical foundations and practicality in mind, we describe a type theory that extends the Calculus of Inductive Constructions featuring observational equality in a universe of strict propositions, with two variants for handling the elimination principle of accessibility predicates: one variant safeguards decidability by sticking to propositional unfolding, and the other variant favors flexibility with definitional unfolding, at the expense of a potentially diverging typechecking procedure. Crucially, the metatheory of this dual approach establishes that any proof made in the definitional variant of the theory can be translated into a proof of the same statement in the propositional variant, all while preserving the decidability of the latter. Moreover, we prove the two variants to be consistent and to satisfy forms of canonicity, ensuring that programs can indeed be properly evaluated. We present an implementation in Rocq and compare it with existing approaches. Overall, this work introduces an effective technique that informs the design of proof assistants with strict propositions, enabling local computation with accessibility predicates without compromising the ambient type theory.

Cite As Get BibTex

Thiago Felicissimo, Yann Leray, Loïc Pujet, Nicolas Tabareau, Éric Tanter, and Théo Winterhalter. Definitional Proof Irrelevance Made Accessible. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 41:1-41:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.41

Author Details

Thiago Felicissimo
  • Inria (Gallinette), Nantes, France
Yann Leray
  • Inria (Gallinette), Nantes, France
Loïc Pujet
  • ICube, Université de Strasbourg, France
Nicolas Tabareau
  • Inria (Gallinette), Nantes, France
Éric Tanter
  • PLEIAD, Computer Science Department, University of Chile, Santiago, Chile
  • Inria (Gallinette), Nantes, France
Théo Winterhalter
  • Inria (Deducteam), Gif-sur-Yvette, France

Acknowledgements

The authors would like to thank the reviewers for their helpful comments.

Supplementary Materials

References

  1. Andreas Abel and Thierry Coquand. Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. Logical Methods in Computer Science, Volume 16, Issue 2, June 2020. URL: https://doi.org/10.23638/LMCS-16(2:14)2020.
  2. Andreas Abel, Thierry Coquand, and Miguel Pagano. A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Logical Methods in Computer Science, 7, 2011. URL: https://doi.org/10.2168/LMCS-7(2:4)2011.
  3. Andreas Abel, Nils Anders Danielsson, and Oskar Eriksson. A graded modal dependent type theory with a universe and erasure, formalized. Proc. ACM Program. Lang., 7(ICFP), 2023. URL: https://doi.org/10.1145/3607862.
  4. Andreas Abel, Joakim Öhman, and Andrea Vezzosi. Decidability of conversion for type theory in type theory. Proceedings of the ACM on Programming Languages, 2(POPL):23:1-23:29, January 2018. URL: https://doi.org/10.1145/3158111.
  5. Peter Aczel. An introduction to inductive definitions. In Jon Barwise, editor, HANDBOOK OF MATHEMATICAL LOGIC, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 739-782. Elsevier, 1977. URL: https://doi.org/10.1016/S0049-237X(08)71120-0.
  6. Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, and Loïc Pujet. Martin-löf à la coq. In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pages 230-245. ACM, 2024. URL: https://doi.org/10.1145/3636501.3636951.
  7. T. Altenkirch. Extensional equality in intensional type theory. In Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pages 412-420, 1999. URL: https://doi.org/10.1109/LICS.1999.782636.
  8. Thorsten Altenkirch. Extensional equality in intensional type theory. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, LICS '99, page 412, USA, 1999. IEEE Computer Society. Google Scholar
  9. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016. Google Scholar
  10. Thorsten Altenkirch, Conor McBride, and Wouter Swierstra. Observational equality, now! In Proceedings of the Workshop on Programming Languages meets Program Verification (PLPV 2007), pages 57-68, 2007. URL: https://doi.org/10.1145/1292597.1292608.
  11. Robert Atkey. Simplified observational type theory, 2018. Implementation at URL: https://github.com/bobatkey/sott.
  12. Jeremy Avigad, Leonardo de Moura, Soonho Kong, Sebastian Ullrich, and with contributions from the Lean Community. Theorem Proving in Lean 4, 2025. URL: https://lean-lang.org/theorem_proving_in_lean4/.
  13. Gilles Barthe. The relevance of proof-irrelevance. In Kim G. Larsen, Sven Skyum, and Glynn Winskel, editors, Automata, Languages and Programming, pages 755-768, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFB0055099.
  14. Valentin Blot. Normalization of System F, formalized in Coq, 2022. URL: https://gitlab.inria.fr/-/snippets/797.
  15. Guillaume Brunerie, Menno de Boer, Peter LeFanu Lumsdaine, and Anders Mörtberg. A formalization of the initiality conjecture in agda. Slides from a talk about joint work with Menno de Boer, Peter Lumsdaine, and Anders Mörtberg, at HoTT, Pittsburgh, CMU, 2019. Google Scholar
  16. Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter. The taming of the rew: A type theory with computational assumptions. Proc. ACM Program. Lang., 5(POPL), 2021. URL: https://doi.org/10.1145/3434341.
  17. Thierry Coquand. Reduction free normalisation for a proof irrelevant type of propositions. Logical Methods in Computer Science, Volume 19, Issue 3, July 2023. URL: https://doi.org/10.46298/lmcs-19(3:5)2023.
  18. Thiago Felicissimo. Generic bidirectional typing for dependent type theories. ACM Trans. Program. Lang. Syst., 47(1), 2025. URL: https://doi.org/10.1145/3715095.
  19. Yannick Forster, Matthieu Sozeau, and Nicolas Tabareau. Verified extraction from coq to ocaml. Proc. ACM Program. Lang., PLDI, June 2024. URL: https://doi.org/10.1145/3656379.
  20. Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional Proof-Irrelevance without K. Proceedings of the ACM on Programming Languages, 3:1-28, January 2019. URL: https://doi.org/10.1145/3290316.
  21. Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures dans l’arithmétique d’ordre supérieur. Thèse de Doctorat d’État, Université de Paris VII, 1972. Google Scholar
  22. Daniel Gratzer, Jonathan Sterling, and Lars Birkedal. Implementing a modal dependent type theory. Proc. ACM Program. Lang., 3(ICFP), 2019. URL: https://doi.org/10.1145/3341711.
  23. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. J. ACM, 40(1):143-184, January 1993. URL: https://doi.org/10.1145/138027.138060.
  24. Martin Hofmann. Conservativity of equality reflection over intensional type theory. In International Workshop on Types for Proofs and Programs, pages 153-164. Springer, 1995. URL: https://doi.org/10.1007/3-540-61780-9_68.
  25. Junyoung Jang, Antoine Gaulin, Jason Z. S. Hu, and Brigitte Pientka. Mctt: A verified kernel for a proof assistant. Proc. ACM Program. Lang., 9(ICFP), 2025. URL: https://doi.org/10.1145/3747511.
  26. Ambrus Kaposi and Szumi Xie. Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics. In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), volume 299 of Leibniz International Proceedings in Informatics (LIPIcs), pages 10:1-10:24, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2024.10.
  27. Gyesik Lee and Benjamin Werner. Proof-irrelevant model of cc with predicative induction and judgmental equality. Logical Methods in Computer Science, Volume 7, Issue 4, November 2011. URL: https://doi.org/10.2168/LMCS-7(4:5)2011.
  28. Meven Lennon-Bertrand. Complete Bidirectional Typing for the Calculus of Inductive Constructions. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.24.
  29. Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, and Théo Winterhalter. The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. In International Conference on Interactive Theorem Proving (ITP 2024), volume 15th International Conference on Interactive Theorem Proving (ITP 2024), page 18, Tbilisi, Georgia, September 2024. Yves Bertot and Temur Kutsia and Michael Norrish. URL: https://doi.org/10.4230/LIPIcs.ITP.2024.26.
  30. Xavier Leroy. Well-founded recursion done right. In CoqPL 2024: The Tenth International Workshop on Coq for Programming Languages, London, United Kingdom, January 2024. ACM. URL: https://inria.hal.science/hal-04356563.
  31. P. Letouzey. Programmation fonctionnelle certifiée - L'extraction de programmes dans l'assistant Coq. PhD thesis, Université Paris-Sud, July 2004. Google Scholar
  32. Assia Mahboubi, Guillaume Melquiond, and Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals. Journal of Automated Reasoning, 62(2):281-300, February 2019. URL: https://doi.org/10.1007/s10817-018-9463-7.
  33. Per Martin-Löf. An intuitionistic theory of types: Predicative part. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium '73, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. Elsevier, 1975. URL: https://doi.org/10.1016/S0049-237X(08)71945-1.
  34. Bengt Nordström. Terminating general recursion. BIT, 28(3):605-619, 1988. URL: https://doi.org/10.1007/BF01941137.
  35. Steven Obua. Partizan games in isabelle/holzf. In Kamel Barkaoui, Ana Cavalcanti, and Antonio Cerone, editors, Theoretical Aspects of Computing - ICTAC 2006, pages 272-286, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11921240_19.
  36. Nicolas Oury. Extensionality in the calculus of constructions. In International Conference on Theorem Proving in Higher Order Logics, pages 278-293. Springer, 2005. URL: https://doi.org/10.1007/11541868_18.
  37. Christine Paulin-Mohring. Introduction to the Calculus of Inductive Constructions. In Bruno Woltzenlogel Paleo and David Delahaye, editors, All about Proofs, Proofs for All, volume 55 of Studies in Logic (Mathematical logic and foundations). College Publications, January 2015. URL: https://hal.inria.fr/hal-01094195.
  38. Pierre-Marie Pédrot. Russian constructivism in a prefascist theory. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20, pages 782-794, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3373718.3394740.
  39. Loïc Pujet, Yann Leray, and Nicolas Tabareau. Observational Equality Meets CIC. ACM Transactions on Programming Languages and Systems (TOPLAS), 47(2):1-35, April 2025. URL: https://doi.org/10.1145/3719342.
  40. Loïc Pujet and Nicolas Tabareau. Observational Equality: Now For Good. Proceedings of the ACM on Programming Languages, 6(POPL):1-29, January 2022. URL: https://doi.org/10.1145/3498693.
  41. Loïc Pujet and Nicolas Tabareau. Impredicative Observational Equality. Proceedings of the ACM on Programming Languages, 7(POPL):74, January 2023. URL: https://doi.org/10.1145/3571739.
  42. Amin Timany and Matthieu Sozeau. Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC). Research Report RR-9105, KU Leuven, Belgium ; Inria Paris, October 2017. Version 2 fixes some typos from version 1.Version 3 fixes a typo in a typing rule from version 2. URL: https://inria.hal.science/hal-01615123.
  43. Taichi Uemura. Abstract and concrete type theories. PhD thesis, University of Amsterdam, 2021. Google Scholar
  44. Benjamin Werner. On the strength of proof-irrelevant type theories. Logical Methods in Computer Science, 4:1-20, September 2008. URL: https://doi.org/10.2168/LMCS-4(3:13)2008.
  45. Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau. Eliminating reflection from type theory. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, pages 91-103, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3293880.3294095.
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact