Document Open Access Logo

What Does It Take to Certify a Conversion Checker?

Author Meven Lennon-Bertrand

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.27.pdf
  • Filesize: 0.79 MB
  • 23 pages
HTML5 Logo HTML (experimental)
LIPIcs.FSCD.2025.27.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Type structures
  • Software and its engineering → Data types and structures
Keywords
  • Dependent types
  • Bidirectional typing
  • Certified software

Metrics

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

Abstract

We report on a detailed exploration of the properties of conversion (definitional equality) in dependent type theory, with the goal of certifying decision procedures for it. While in that context the property of normalisation has attracted the most light, we instead emphasize the importance of injectivity properties, showing that they alone are both crucial and sufficient to certify most desirable properties of conversion checkers. We also explore the certification of a fully untyped conversion checker, with respect to a typed specification, and show that the story is mostly unchanged, although the exact injectivity properties needed are subtly different.

Cite As Get BibTex

Meven Lennon-Bertrand. What Does It Take to Certify a Conversion Checker?. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.27

Author Details

Meven Lennon-Bertrand
  • University of Cambridge, UK

Funding

This work was supported in part by a European Research Council (ERC) Consolidator Grant for the project "TypeFoundry", funded under the European Union’s Horizon 2020 Framework Programme (grant agreement no. 101002277).

Acknowledgements

Many thanks to Kenji Maillard and Thibaut Benjamin for their feedback on drafts of this paper, and to the anonymous reviewers for their helpful comments.

Supplementary Materials

References

  1. Andreas Abel and Thorsten Altenkirch. A partial type checking algorithm for type:type. Electronic Notes in Theoretical Computer Science, 229(5):3-17, 2011. Proceedings of the Second Workshop on Mathematically Structured Functional Programming (MSFP 2008). URL: https://doi.org/10.1016/j.entcs.2011.02.013.
  2. Andreas Abel and Thierry Coquand. Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. Fundamenta Informaticae, 77(4):345-395, 2007. TLCA'05 special issue. URL: http://fi.mimuw.edu.pl/abs77.html#15.
  3. Andreas Abel, Joakim Öhman, and Andrea Vezzosi. Decidability of conversion for type theory in type theory. Proc. ACM Program. Lang., 2(POPL), December 2017. URL: https://doi.org/10.1145/3158111.
  4. Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, and Thomas Sewell. Candle: A Verified Implementation of HOL Light. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving (ITP 2022), volume 237 of Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.3.
  5. Robin Adams. Pure type systems with judgemental equality. J. Funct. Program., 16(2):219-246, 2006. URL: https://doi.org/10.1017/S0956796805005770.
  6. Arthur Adjedj. Issue #2258: Defeq transitivity failures for eta. GitHub issue. URL: https://github.com/leanprover/lean4/issues/2258.
  7. Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, and Loïc Pujet. Martin-löf à la coq. In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, pages 230-245, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3636501.3636951.
  8. Antoine Allioux. Issue #5174: Rewrite rules and eta-expansion of the unit type. GitHub issue. URL: https://github.com/agda/agda/issues/5174.
  9. Henk Barendregt and Herman Geuvers. Proof-assistants using dependent type systems. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, Handbook of Automated Reasoning, pages 1149-1238. North-Holland, Amsterdam, 2001. URL: https://doi.org/10.1016/B978-044450813-3/50020-5.
  10. Bruno Barras and Benjamin Werner. Coq in coq. Unpublished manuscript, 1997. URL: http://www.lix.polytechnique.fr/Labo/Bruno.Barras/publi/coqincoq.pdf.
  11. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. The hott library: a formalization of homotopy type theory in coq. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 164-172. Association for Computing Machinery, 2017. URL: https://doi.org/10.1145/3018610.3018615.
  12. 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, 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.
  13. Mario Carneiro. Lean4lean: Towards a formalized metatheory for the lean theorem prover, March 2024. URL: https://doi.org/10.48550/arXiv.2403.14064.
  14. Jesper Cockx. Issue #3785: Comparison of blocked terms doesn't respect eta. GitHub issue. URL: https://github.com/agda/agda/issues/3785.
  15. Jesper Cockx. Issue #5837: Occurs check does not properly handle singleton type. GitHub issue. URL: https://github.com/agda/agda/issues/5837.
  16. Thierry Coquand. An algorithm for type-checking dependent types. Science of Computer Programming, 26(1), 1996. URL: https://doi.org/10.1016/0167-6423(95)00021-6.
  17. Thierry Coquand and Simon Huber. An adequacy theorem for dependent type theory. Theory of Computing Systems, 63(4):647-665, July 2018. URL: https://doi.org/10.1007/s00224-018-9879-9.
  18. Nathanaëlle Courant. Towards an efficient and formally verified convertibility checker. PhD thesis, Université Paris Cité, 2024. Google Scholar
  19. Adrian Dapprich. Generating Infrastructural Code for Terms with Binders using MetaCoq and OCaml. Bachelor thesis, Saarland University, 2021. Google Scholar
  20. Jana Dunfield and Neel Krishnaswami. Bidirectional typing. ACM Computing Surveys, 54(5), May 2021. URL: https://doi.org/10.1145/3450952.
  21. Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional proof-irrelevance without k. Proceedings of the ACM on Programming Languages, 3(POPL):1-28, January 2019. URL: https://doi.org/10.1145/329031610.1145/3290316.
  22. Gaëtan Gilbert. A type theory with definitional proof-irrelevance. PhD thesis, Université de Nantes, 2020. Google Scholar
  23. Jason Z. S. Hu, Junyoung Jang, and Brigitte Pientka. Normalization by evaluation for modal dependent type theory. Journal of Functional Programming, 33, 2023. URL: https://doi.org/10.1017/S0956796823000060.
  24. Junyoung Jang, Jason Z. S. Hu, Antoine Gaulin, and Brigitte Pientka. Mctt: Building a correct-by-construction proof checkerfor martin-löf type theory. In 4th Workshop on the Implementation of Type Systems, 2025. Google Scholar
  25. Ambrus Kaposi. Issue #6417: Forward declaration breaks eta for unit type. GitHub issue. URL: https://github.com/agda/agda/issues/6417.
  26. Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. Constructing quotient inductive-inductive types. Proceeding of the ACM on Programming Languages, 3(POPL), January 2019. URL: https://doi.org/10.1145/3290315.
  27. András Kovács. Efficient evaluation with controlled definition unfolding. In 3rd Workshop on the Implementation of Type Systems, 2024. Google Scholar
  28. András Kovács. Eta conversion for the unit type (is still not that simple). In 4th Workshop on the Implementation of Type Systems, 2025. Google Scholar
  29. Meven Lennon-Bertrand. LogRel-Coq – FSCD 2025. Software, version fscd25., (visited on 2025-06-23). URL: https://github.com/CoqHott/logrel-coq/tree/fscd25
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.23665
  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), 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.
  31. Meven Lennon-Bertrand. Bidirectional Typing for the Calculus of Inductive Constructions. phdthesis, Nantes Université, 2022. Google Scholar
  32. Meven Lennon-Bertrand. Equivalence between typed and untyped algorithmic conversions. In 28th International Conference on Types for Proofs and Programs, June 2022. URL: https://types22.inria.fr/programme/.
  33. Meven Lennon-Bertrand. À bas l'η - Coq’s troublesome η-conversion. In 1st Workshop on the Implementation of Type Systems, 2022. Google Scholar
  34. Meven Lennon-Bertrand. What does it take to certify conversion?, 2025. URL: https://doi.org/10.48550/arXiv.2502.15500.
  35. Meven Lennon-Bertrand and Neel Krishnaswami. Decidable type-checking for bidirectional martin-löf type theory. In 29th International Conference on Types for Proofs and Programs, 2023. URL: https://types2023.webs.upv.es/.
  36. Yann Leray. Formalisation et implémentation des propositions strictes dans MetaCoq. Technical report, Inria Rennes - Bretagne Atlantique ; LS2N-Nantes Université, August 2022. URL: https://inria.hal.science/hal-04433492.
  37. Bohdan Liesnikov and Jesper Cockx. Building a correct-by-construction type checker for a dependently typed core language. In Oleg Kiselyov, editor, Programming Languages and Systems, pages 63-83, Singapore, 2025. Springer Nature Singapore. Google Scholar
  38. Yiyun Liu, Jonathan Chan, and Stephanie Weirich. Consistency of a dependent calculus of indistinguishability. Proceeding of the ACM of Programming Languages, 9(POPL), January 2025. URL: https://doi.org/10.1145/3704843.
  39. Peter LeFanu Lumsdaine, Guillaume Brunerie, Menno de Boer, and Anders Mörtberg. Initiality for martin-löf type theory. Talk at the HoTTest seminar, 2020. Google Scholar
  40. Per Martin-Löf and Giovanni Sambin. Intuitionistic Type Theory. Number 1 in Studies in Proof Theory. Napoli: Bibliopolis, 1984. Google Scholar
  41. Conor McBride. Turing-completeness totally free. In Ralf Hinze and Janis Voigtländer, editors, Mathematics of Program Construction, pages 257-275, Cham, 2015. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-19797-5_13.
  42. Conor McBride. Basics of bidirectionalism. Blog post, August 2018. URL: https://pigworker.wordpress.com/2018/08/06/basics-of-bidirectionalism/.
  43. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, September 2007. Google Scholar
  44. Vincent Siles and Hugo Herbelin. Pure type system conversion is always typable. J. Funct. Program., 22(2):153-180, 2012. URL: https://doi.org/10.1017/S0956796812000044.
  45. Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Nielsen, Nicolas Tabareau, and Théo Winterhalter. Correct and complete type checking and certified erasure for coq, in coq. Journal of the ACM, November 2024. URL: https://doi.org/10.1145/3706056.
  46. Kathrin Stark. Mechanising syntax with binders in Coq. PhD thesis, Saarland University, Saarbrücken, Germany, 2020. URL: https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/28822.
  47. Jonathan Sterling. First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. PhD thesis, Carnegie Mellon University, November 2021. Doctoral thesis of Jonathan Sterling, Carnegie Mellon University. URL: https://doi.org/10.5281/zenodo.6990769.
  48. Kristian Stoevring. Extending the extensional lambda calculus with surjective pairing is conservative. Logical Methods in Computer Science, Volume 2, Issue 2, 2006. URL: https://doi.org/10.2168/LMCS-2(2:1)2006.
  49. M. Takahashi. Parallel reductions in λ-calculus. Information and Computation, 118(1):120-127, 1995. URL: https://doi.org/10.1006/inco.1995.1057.
  50. The Coq Development Team. The coq proof assistant, June 2024. URL: https://doi.org/10.5281/zenodo.14542673.
  51. Pawel 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.
  52. Théo Winterhalter. Formalisation and meta-theory of type theory. PhD thesis, Université de Nantes, 2020. Google Scholar
  53. Théo Winterhalter. Composable partial functions in Coq, totally for free. In 29th International Conference on Types for Proofs and Programs, 2023. Google Scholar
  54. Andrew Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38-94, 1994. URL: https://doi.org/10.1006/inco.1994.1093.
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