Document Open Access Logo

Panbench: A Comparative Benchmarking Tool for Dependently-Typed Languages

Authors Reed Mullanix , Jacques Carette

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.17.pdf
  • Filesize: 1.51 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Mathematical software performance
Keywords
  • Benchmarking
  • dependent types
  • testing

Metrics

Abstract

We benchmark four proof assistants (Agda, Idris 2, Lean 4 and Rocq) through a single test suite. We focus our benchmarks on the basic features that all systems based on a similar foundations (dependent type theory) have in common. We do this by creating an "over language" in which to express all the information we need to be able to output correct and idiomatic syntax for each of our targets. Our benchmarks further focus on "basic engineering" of these systems: how do they handle long identifiers, long lines, large records, large data declarations, and so on.
Our benchmarks reveals both flaws and successes in all systems. We give a thorough analysis of the results.
We also detail the design of our extensible system. It is designed so that additional tests and additional system versions can easily be added. A side effect of this work is a better understanding of the common abstract syntactic structures of all four systems.

Cite As Get BibTex

Reed Mullanix and Jacques Carette. Panbench: A Comparative Benchmarking Tool for Dependently-Typed Languages. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.17

Author Details

Reed Mullanix
  • Department of Computing and Software, McMaster University, Hamilton, Canada
Jacques Carette
  • Department of Computing and Software, McMaster University, Hamilton, Canada

Supplementary Materials

References

  1. Agda Developers. Agda. URL: https://agda.readthedocs.io/.
  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. arXiv:2311.07185 [cs], November 2023. URL: https://doi.org/10.48550/arXiv.2311.07185.
  3. Edwin Brady. Idris 2: Quantitative Type Theory in Practice. In Anders Møller and Manu Sridharan, editors, 35th European Conference on Object-Oriented Programming (ECOOP 2021), volume 194 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:26, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2021.9.
  4. Jacques Carette, Oleg Kiselyov, and Chung-Chieh Shan. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. Journal of Functional Programming, 19(5):509-543, September 2009. URL: https://doi.org/10.1017/S0956796809007205.
  5. Thierry Coquand. Pattern matching with dependent types. In Proceedings of the 1992 Workshop on Types for Proofs and Programs, 1992. Google Scholar
  6. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings, pages 625-635, Berlin, Heidelberg, 2021. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  7. Eelco Dolstra and The Nix contributors. Nix. URL: https://github.com/NixOS/nix.
  8. R. Kent Dybvig. The development of chez scheme. In Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, ICFP ’06, pages 1-12, New York, NY, USA, 2006. Association for Computing Machinery. URL: https://doi.org/10.1145/1159803.1159805.
  9. February 2026. URL: https://github.com/GrammaticalFramework/informath.
  10. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143-184, January 1993. URL: https://doi.org/10.1145/138027.138060.
  11. Hugo Herbelin, Pierre-Marie Pédrot, coqbot, Gaëtan Gilbert, Maxime Dénès, letouzey, Emilio Jesús Gallego Arias, Matthieu Sozeau, Théo Zimmermann, Enrico Tassi, Jean-Christophe Filliatre, Pierre Roux, Guillaume Melquiond, Arnaud Spiwack, Jason Gross, barras, Pierre Boutillier, Vincent Laporte, Jim Fehrle, Stéphane Glondu, Yves Bertot, Jasper Hugunin, Clément Pit-Claudel, Ali Caglayan, forestjulien, Pierre Courtieu, Frédéric Besson, Pierre Rousselin, MSoegtropIMC, and Yann Leray. Rocq, February 2026. URL: https://doi.org/10.5281/zenodo.15149629.
  12. Mark P. Jones. Type classes with functional dependencies. In Gert Smolka, editor, Programming Languages and Systems, pages 230-244, Berlin, Heidelberg, 2000. Springer. URL: https://doi.org/10.1007/3-540-46425-5_15.
  13. Neil Mitchell. Shake before building: replacing make with haskell. SIGPLAN Not., 47(9):55-66, September 2012. URL: https://doi.org/10.1145/2398856.2364538.
  14. Reed Mullanix and Jacques Carette. panbench. Software, (visited on 2026-06-02). URL: https://github.com/JacquesCarette/panbench
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26134
  15. Aarne Ranta. Grammatical framework: programming with multilingual grammars. CSLI studies in computational linguistics. CSLI Publications, Center for the Study of Language and Information, Stanford, Calif, 2011. Google Scholar
  16. Matthieu Sozeau. Equations: A dependent pattern-matching compiler. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving, pages 419-434, Berlin, Heidelberg, 2010. Springer. URL: https://doi.org/10.1007/978-3-642-14052-5_29.
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