Search Results

Documents authored by Mullanix, Reed

Artifact
Software
DOI: 10.4230/artifacts.26134
panbench

Authors: Reed Mullanix and Jacques Carette

Abstract
Cite as

Reed Mullanix, Jacques Carette. panbench (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{Mullanix:2026,
   title = {{panbench}}, 
   author = {Mullanix, Reed and Carette, Jacques},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:1ab8fcd7ff7e56663004064274c3fe86bc213ec3;origin=https://github.com/JacquesCarette/panbench;visit=swh:1:snp:6182348efe3fa4a888a6200c05c0c0970178a16c;anchor=swh:1:rev:c2089c1f2ec9871b3c6ecdfd6ba63fda835298ef}{\texttt{swh:1:dir:1ab8fcd7ff7e56663004064274c3fe86bc213ec3}} (visited on 2026-07-16)},
   url = {https://github.com/JacquesCarette/panbench},
   doi = {10.4230/artifacts.26134},
}
Document
DOI: 10.4230/LIPIcs.ITP.2026.17
Panbench: A Comparative Benchmarking Tool for Dependently-Typed Languages

Authors: Reed Mullanix and Jacques Carette

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{mullanix_et_al:LIPIcs.ITP.2026.17,
  author =	{Mullanix, Reed and Carette, Jacques},
  title =	{{Panbench: A Comparative Benchmarking Tool for Dependently-Typed Languages}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{17:1--17:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.17},
  URN =		{urn:nbn:de:0030-drops-269915},
  doi =		{10.4230/LIPIcs.ITP.2026.17},
  annote =	{Keywords: Benchmarking, dependent types, testing}
}
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