Document Open Access Logo

Divide and Check: Logical Relations, No Algorithms Attached

Authors Josselin Poiret , Kenji Maillard , Nicolas Tabareau

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.26.pdf
  • Filesize: 0.83 MB
  • 23 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Type Theory
  • Proof Assistants

Metrics

Abstract

The correctness of type-checking implementations for proof assistants based on dependent type theory relies on metatheoretical properties that ensure the decidability of typing, some of which require substantial logical strength. Recent mechanizations of such algorithms have highlighted the importance of separating the algorithmic components of the proof - often intricate but requiring relatively low logical strength - from the logical components, which depend on stronger metatheoretical properties, such as normalization or the injectivity of type constructors. In this work, we revisit the logical relations technique and show how it can be used to derive these metatheoretical properties in a direct and uniform way for a core dependent type theory featuring Π-types, N, ⊥ and a universe U. Our presentation yields a compact and conceptually simplified argument that isolates the logically strong reasoning from the algorithmic core. We argue that this approach scales smoothly to richer type theories, and demonstrate this by extending our construction to Exceptional Type Theory (ExcTT), obtaining the first mechanized canonicity proof for this theory.

Cite As Get BibTex

Josselin Poiret, Kenji Maillard, and Nicolas Tabareau. Divide and Check: Logical Relations, No Algorithms Attached. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 26:1-26:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.26

Author Details

Josselin Poiret
  • Nantes Université, École Centrale Nantes, CNRS, INRIA, LS2N, UMR 6004, Nantes, France
Kenji Maillard
  • Inria, Nantes, France
Nicolas Tabareau
  • Inria, Nantes, France

Acknowledgements

The authors want to thank Thiago Felicissimo for their many suggestions, and Rafaël Bocquet and Yann Leray for valuable discussions.

Supplementary Materials

References

  1. Andreas Abel. Normalization by Evaluation: Dependent Types and Impredicativity. Habilitation thesis, Institut für Informatik, Ludwig-Maximilians-Universität München, 2013. Google Scholar
  2. 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):920-954, 2023. URL: https://doi.org/10.1145/3607862.
  3. Andreas Abel, Joakim Öhman, and Andrea Vezzosi. Decidability of conversion for type theory in type theory. Proc. ACM Program. Lang., 2(POPL):23:1-23:29, 2018. URL: https://doi.org/10.1145/3158111.
  4. 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.
  5. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction free normalization proof. In David H. Pitt, David E. Rydeheard, and Peter T. Johnstone, editors, Category Theory and Computer Science, 6th International Conference, CTCS '95, Cambridge, UK, August 7-11, 1995, Proceedings, volume 953 of Lecture Notes in Computer Science, pages 182-199. Springer, 1995. URL: https://doi.org/10.1007/3-540-60164-3_27.
  6. Thorsten Altenkirch and Ambrus Kaposi. Normalisation by evaluation for type theory, in type theory. Log. Methods Comput. Sci., 13(4), 2017. URL: https://doi.org/10.23638/LMCS-13(4:1)2017.
  7. Martin Baillon, Assia Mahboubi, and Pierre-Marie Pédrot. In Cantor space no one can hear you stream. In Robbert Krebbers, editor, Programming Languages and Systems - 35th European Symposium on Programming, ESOP 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part I, Lecture Notes in Computer Science, pages 72-103. Springer, 2026. URL: https://doi.org/10.1007/978-3-032-22720-1_4.
  8. Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed lambda-calculus. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), Amsterdam, The Netherlands, July 15-18, 1991, pages 203-211. IEEE Computer Society, 1991. URL: https://doi.org/10.1109/LICS.1991.151645.
  9. Rafaël Bocquet, Ambrus Kaposi, and Christian Sattler. For the metatheory of type theory, internal sconing is enough. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, Rome, Italy, July 3-6, 2023, volume 260 of LIPIcs, pages 18:1-18:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.FSCD.2023.18.
  10. Mathis Bouverot-Dupuis, Théo Winterhalter, Kenji Maillard, and Kathrin Stark. Sulfur: Substitution generation using a logical framework. 15m talk in RocqPL session; extended abstract available, January 2026. Google Scholar
  11. Guillaume Brunerie and Menno Gilbers. initiality. https://github.com/guillaumebrunerie/initiality/tree/master, 2020.
  12. Mario Carneiro. Lean4Lean: Towards a formalized metatheory for the Lean theorem prover. CoRR, abs/2403.14064, 2024. URL: https://doi.org/10.48550/arXiv.2403.14064.
  13. François Conduché. Algèbre des catégories. - au sujet de l'existence d'adjoints à droite aux foncteurs "image réciproque" dans la catégorie des catégories. Comptes rendus hebdomadaires des séances de l'Académie des sciences. Séries A et B, Sciences mathématiques et Sciences physiques, Académie des sciences (France), 1972. Public domain. 1972/11/06 (SERA-B,T275,N19). Ark identifier: ark:/12148/bpt6k56191352. Source: Archives de l'Académie des sciences. Provenance: Bibliothèque nationale de France. Online since 2010-12-01. URL: http://catalogue.bnf.fr/ark:/12148/cb34416987n.
  14. Thierry Coquand. An algorithm for type-checking dependent types. Sci. Comput. Program., 26(1-3):167-177, 1996. URL: https://doi.org/10.1016/0167-6423(95)00021-6.
  15. Thierry Coquand. Canonicity and normalization for dependent type theory. Theor. Comput. Sci., 777:184-191, 2019. URL: https://doi.org/10.1016/J.TCS.2019.01.015.
  16. Thierry Coquand. Reduction free normalisation for a proof irrelevant type of propositions. Log. Methods Comput. Sci., 19(3), 2023. URL: https://doi.org/10.46298/LMCS-19(3:5)2023.
  17. Nils Anders Danielsson, Naïm Camille Favier, and Ondřej Kubánek. Normalisation for first-class universe levels. Proc. ACM Program. Lang., 10(POPL), 2026. URL: https://doi.org/10.1145/3776645.
  18. Peter Dybjer and Anton Setzer. Indexed induction-recursion. J. Log. Algebraic Methods Program., 66(1):1-49, 2006. URL: https://doi.org/10.1016/J.JLAP.2005.07.001.
  19. Marcelo Fiore. Semantic analysis of normalisation by evaluation for typed lambda calculus. Math. Struct. Comput. Sci., 32(8):1028-1065, 2022. URL: https://doi.org/10.1017/S0960129522000263.
  20. Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional proof-irrelevance without K. Proc. ACM Program. Lang., 3(POPL):3:1-3:28, 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. PhD thesis, Université Paris VII, June 1972. Google Scholar
  22. Jean Giraud. Méthode de la descente. Bulletin de la Société mathématique de France, Mémoire(2):156, 1964. URL: https://doi.org/10.24033/msmf.2.
  23. Daniel Gratzer. Normalization for multimodal type theory. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 2:1-2:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3532398.
  24. Peter G. Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta, and Thorsten Altenkirch. Small induction recursion. In Masahito Hasegawa, editor, Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings, volume 7941 of Lecture Notes in Computer Science, pages 156-172. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38946-7_13.
  25. Jason Z. S. Hu, Junyoung Jang, and Brigitte Pientka. Normalization by evaluation for modal dependent type theory. J. Funct. Program., 33, 2023. URL: https://doi.org/10.1017/S0956796823000060.
  26. Junyoung Jang, Antoine Gaulin, Jason Z. S. Hu, and Brigitte Pientka. McTT: A verified kernel for a proof assistant. Proc. ACM Program. Lang., 2025. URL: https://doi.org/10.1145/3747511.
  27. Ambrus Kaposi. Towards quotient inductive-inductive-recursive types. TYPES, 2023, 2023. URL: https://types2023.webs.upv.es/TYPES2023.pdf.
  28. Ambrus Kaposi and Loïc Pujet. Type theory in type theory using a strictified syntax. Proc. ACM Program. Lang., 9(ICFP), 2025. URL: https://doi.org/10.1145/3747535.
  29. Carl Krary. The Istari proof assistant. URL: https://istarilogic.org/.
  30. 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, Rome, Italy (Virtual Conference), June 29 - July 1, 2021, volume 193 of LIPIcs, pages 24:1-24:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.24.
  31. Meven Lennon-Bertrand. What does it take to certify a conversion checker? In Maribel Fernández, editor, 10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025, July 14-20, 2025, Birmingham, UK, volume 337 of LIPIcs, pages 27:1-27:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.FSCD.2025.27.
  32. Runming Li, Yue Yao, and Robert Harper. Mechanizing synthetic Tait computability in Istari. In Kathrin Stark, Yannick Zakowski, Nikhil Swamy, and Nicolas Tabareau, editors, Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2026, Rennes, France, January 12-13, 2026, pages 231-247. ACM, 2026. URL: https://doi.org/10.1145/3779031.3779085.
  33. Bohdan Liesnikov and Jesper Cockx. Building a correct-by-construction type checker for a dependently typed core language. In Programming Languages and Systems: 22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22-24, 2024, Proceedings, pages 63-83, Berlin, Heidelberg, 2024. Springer-Verlag. URL: https://doi.org/10.1007/978-981-97-8943-6_4.
  34. Yiyun Liu and Stephanie Weirich. Algorithmic conversion with surjective pairing: A syntactic and untyped approach. Proc. ACM Program. Lang., 10(POPL), 2026. URL: https://doi.org/10.1145/3776672.
  35. Per Martin-Löf. An intuitionistic theory of types. In Giovanni Sambin and Jan M. Smith, editors, Twenty Five Years of Constructive Type Theory, pages 127-172. Clarendon Press, 1998. Also known as MLTT72, published version of an unpublished 1972 note. Google Scholar
  36. Pierre-Marie Pédrot. `Upon this quote I will build my Church thesis'. Commun. ACM, 68(6):75-83, 2025. URL: https://doi.org/10.1145/3715707.
  37. Pierre-Marie Pédrot and Nicolas Tabareau. Failure is not an option - an exceptional type theory. In Amal Ahmed, editor, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10801 of Lecture Notes in Computer Science, pages 245-271. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89884-1_9.
  38. Pierre-Marie Pédrot, Nicolas Tabareau, Hans Jacob Fehrmann, and Éric Tanter. A reasonably exceptional type theory. Proc. ACM Program. Lang., 3(ICFP):108:1-108:29, 2019. URL: https://doi.org/10.1145/3341712.
  39. Josselin Poiret, Gaëtan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, and Éric Tanter. All your base are belong to 𝒰_s: Sort polymorphism for proof assistants. Proceedings of the ACM on Programming Languages, 9(POPL):76:1-76:29, 2025. URL: https://doi.org/10.1145/3704912.
  40. Loïc Pujet, Yann Leray, and Nicolas Tabareau. Observational equality meets CIC. ACM Trans. Program. Lang. Syst., 47(2):6:1-6:35, 2025. URL: https://doi.org/10.1145/3719342.
  41. Loïc Pujet and Nicolas Tabareau. Observational equality: now for good. Proc. ACM Program. Lang., 6(POPL):1-27, 2022. URL: https://doi.org/10.1145/3498693.
  42. Loïc Pujet and Nicolas Tabareau. Observational equality meets CIC. In Stephanie Weirich, editor, Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14576 of Lecture Notes in Computer Science, pages 275-301. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57262-3_12.
  43. Johann Rosain, Tomás Díaz, Kenji Maillard, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter, and Théo Winterhalter. Bounded sort polymorphism with elimination constraints. In Proceedings of the 2026 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM, 2026. URL: https://doi.org/10.1145/3776732.
  44. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. The MetaCoq Project. Journal of Automated Reasoning, February 2020. URL: https://doi.org/10.1007/s10817-019-09540-0.
  45. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. Coq coq correct! Verification of type checking and erasure for Coq, in Coq. Proceedings of the ACM on Programming Languages, 4(POPL), December 2019. URL: https://doi.org/10.1145/3371076.
  46. Matthieu Sozeau and Cyprien Mangin. Equations reloaded: high-level dependently-typed functional programming and proving in Coq. Proc. ACM Program. Lang., 2019. URL: https://doi.org/10.1145/3341690.
  47. Kathrin Stark, Steven Schäfer, and Jonas Kaiser. Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. In Assia Mahboubi and Magnus O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pages 166-180. ACM, 2019. URL: https://doi.org/10.1145/3293880.3294101.
  48. Jonathan Sterling. First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. PhD thesis, Carnegie Mellon University, 2021. Version 1.1, revised May 2022. URL: https://doi.org/10.5281/zenodo.6990769.
  49. Jonathan Sterling and Carlo Angiuli. Normalization for cubical type theory. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-15. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470719.
  50. William W. Tait. Intensional interpretations of functionals of finite type I. J. Symb. Log., 32(2):198-212, 1967. URL: https://doi.org/10.2307/2271658.
  51. Paweł Wieczorek and Dariusz Biernacki. A Coq formalization of normalization by evaluation for Martin-Löf type theory. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pages 266-279, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3167091.
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