Search Results

Documents authored by Carette, Jacques

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}
}
Document
DOI: 10.4230/OASIcs.EVCS.2023.7
Generating Software for Well-Understood Domains

Authors: Jacques Carette, Spencer W. Smith, and Jason Balaci

Published in: OASIcs, Volume 109, Eelco Visser Commemorative Symposium (EVCS 2023)

Abstract
Current software development is often quite code-centric and aimed at short-term deliverables, due to various contextual forces (such as the need for new revenue streams from many individual buyers). We're interested in software where different forces drive the development. Well understood domains and long-lived software provide one such context. A crucial observation is that software artifacts that are currently handwritten contain considerable duplication. By using domain-specific languages and generative techniques, we can capture the contents of many of the artifacts of such software. Assuming an appropriate codification of domain knowledge, we find that the resulting de-duplicated sources are shorter and closer to the domain. Our prototype, Drasil, indicates improvements to traceability and change management. We're also hopeful that this could lead to long-term productivity improvements for software where these forces are at play.
Cite as

Jacques Carette, Spencer W. Smith, and Jason Balaci. Generating Software for Well-Understood Domains. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 7:1-7:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{carette_et_al:OASIcs.EVCS.2023.7,
  author =	{Carette, Jacques and Smith, Spencer W. and Balaci, Jason},
  title =	{{Generating Software for Well-Understood Domains}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{7:1--7:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-267-9},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{109},
  editor =	{L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.7},
  URN =		{urn:nbn:de:0030-drops-177776},
  doi =		{10.4230/OASIcs.EVCS.2023.7},
  annote =	{Keywords: code generation, document generation, knowledge capture, software engineering}
}
Document
DOI: 10.4230/OASIcs.EVCS.2023.19
Eelco Visser as a Founding Member of the IFIP WG 2.11

Authors: Christian Lengauer and Jacques Carette

Published in: OASIcs, Volume 109, Eelco Visser Commemorative Symposium (EVCS 2023)

Abstract
Appreciation of Eelco Visser’s contribution to the IFIP WG 2.11 by two of its chairs. Christian Lengauer was chair from 2007 to 2013. Jacques Carette has been chair since 2019.
Cite as

Christian Lengauer and Jacques Carette. Eelco Visser as a Founding Member of the IFIP WG 2.11. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 19:1-19:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{lengauer_et_al:OASIcs.EVCS.2023.19,
  author =	{Lengauer, Christian and Carette, Jacques},
  title =	{{Eelco Visser as a Founding Member of the IFIP WG 2.11}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{19:1--19:3},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-267-9},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{109},
  editor =	{L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.19},
  URN =		{urn:nbn:de:0030-drops-177891},
  doi =		{10.4230/OASIcs.EVCS.2023.19},
  annote =	{Keywords: IFIP WG 2.11}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2021.4
A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory

Authors: William DeMeo and Jacques Carette

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

Abstract
The Agda Universal Algebra Library is a project aimed at formalizing the foundations of universal algebra, equational logic and model theory in dependent type theory using Agda. In this paper we draw from many components of the library to present a self-contained, formal, constructive proof of Birkhoff’s HSP theorem in Martin-Löf dependent type theory. This achieves one of the project’s initial goals: to demonstrate the expressive power of inductive and dependent types for representing and reasoning about general algebraic and relational structures by using them to formalize a significant theorem in the field.
Cite as

William DeMeo and Jacques Carette. A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{demeo_et_al:LIPIcs.TYPES.2021.4,
  author =	{DeMeo, William and Carette, Jacques},
  title =	{{A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-L\"{o}f Type Theory}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-254-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{239},
  editor =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.4},
  URN =		{urn:nbn:de:0030-drops-167737},
  doi =		{10.4230/LIPIcs.TYPES.2021.4},
  annote =	{Keywords: Agda, constructive mathematics, dependent types, equational logic, formal verification, Martin-L\"{o}f type theory, model theory, universal algebra}
}
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