Search Results

Documents authored by Cockx, Jesper

Document
DOI: 10.4230/LIPIcs.ITP.2026.5
Enhancing Interactive Theorem Prover Error Messages with Hints

Authors: Maria Khakimova, Sára Juhošová, Jaro Reinders, and Jesper Cockx

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

Abstract
Interactive theorem provers (ITPs) are promising tools for ensuring program correctness, but users often complain about their poor usability and steep learning curve. A common complaint, especially among new users, are confusing error messages that expose details of the ITP’s underlying theory or implementation details. In this work, we investigate how adding hints to three types of scope and type checking error messages in the Agda ITP affects the new users' debugging experience. We evaluate the effectiveness and perceived helpfulness of those error messages by conducting a between-subjects user study where we provide a series of Agda code snippets, each containing a single error that the participants have to fix based on the error message. We measure the success rate, time taken to fix the error, and perceived helpfulness for each code snippet with the original as well as the enhanced error message and determine the statistical significance of adding the hint. Our results show that correct hints can improve the success rate and time taken to fix the error, and that error messages with hints are rated significantly more helpful than those without. Additionally, we find that while error messages with incorrect hints are often rated as more misleading, they do not significantly impact the success rate or time taken to fix the error. These results show that adding hints to error messages is a viable step on the path towards making ITPs more widely accessible.
Cite as

Maria Khakimova, Sára Juhošová, Jaro Reinders, and Jesper Cockx. Enhancing Interactive Theorem Prover Error Messages with Hints. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{khakimova_et_al:LIPIcs.ITP.2026.5,
  author =	{Khakimova, Maria and Juho\v{s}ov\'{a}, S\'{a}ra and Reinders, Jaro and Cockx, Jesper},
  title =	{{Enhancing Interactive Theorem Prover Error Messages with Hints}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{5:1--5:19},
  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.5},
  URN =		{urn:nbn:de:0030-drops-269791},
  doi =		{10.4230/LIPIcs.ITP.2026.5},
  annote =	{Keywords: Agda, error messages, hints, new users}
}
Document
DOI: 10.4230/OASIcs.EVCS.2023.6
Dependently Typed Languages in Statix

Authors: Jonathan Brouwer, Jesper Cockx, and Aron Zwaan

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

Abstract
Static type systems can greatly enhance the quality of programs, but implementing a type checker that is both expressive and user-friendly is challenging and error-prone. The Statix meta-language (part of the Spoofax language workbench) aims to make this task easier by automatically deriving a type checker from a declarative specification of a type system. However, so far Statix has not been used to implement dependent types, which is a class of type systems which require evaluation of terms during type checking. In this paper, we present an implementation of a simple dependently typed language in Statix, and discuss how to extend it with several common features such as inductive data types, universes, and inference of implicit arguments. While we encountered some challenges in the implementation, our conclusion is that Statix is already usable as a tool for implementing dependent types.
Cite as

Jonathan Brouwer, Jesper Cockx, and Aron Zwaan. Dependently Typed Languages in Statix. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 6:1-6:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{brouwer_et_al:OASIcs.EVCS.2023.6,
  author =	{Brouwer, Jonathan and Cockx, Jesper and Zwaan, Aron},
  title =	{{Dependently Typed Languages in Statix}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{6:1--6:8},
  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.6},
  URN =		{urn:nbn:de:0030-drops-177769},
  doi =		{10.4230/OASIcs.EVCS.2023.6},
  annote =	{Keywords: Spoofax, Statix, Dependent Types, Scope Graphs, Calculus of Constructions}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.TYPES.2021
LIPIcs, Volume 239, TYPES 2021, Complete Volume

Authors: Henning Basold, Jesper Cockx, and Silvia Ghilezan

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

Abstract
LIPIcs, Volume 239, TYPES 2021, Complete Volume
Cite as

27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 1-280, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Proceedings{basold_et_al:LIPIcs.TYPES.2021,
  title =	{{LIPIcs, Volume 239, TYPES 2021, Complete Volume}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{1--280},
  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},
  URN =		{urn:nbn:de:0030-drops-167680},
  doi =		{10.4230/LIPIcs.TYPES.2021},
  annote =	{Keywords: LIPIcs, Volume 239, TYPES 2021, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TYPES.2021.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Henning Basold, Jesper Cockx, and Silvia Ghilezan

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

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{basold_et_al:LIPIcs.TYPES.2021.0,
  author =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{0:i--0:viii},
  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.0},
  URN =		{urn:nbn:de:0030-drops-167691},
  doi =		{10.4230/LIPIcs.TYPES.2021.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2019.2
Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules

Authors: Jesper Cockx

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)

Abstract
Dependently typed languages such as Coq and Agda can statically guarantee the correctness of our proofs and programs. To provide this guarantee, they restrict users to certain schemes - such as strictly positive datatypes, complete case analysis, and well-founded induction - that are known to be safe. However, these restrictions can be too strict, making programs and proofs harder to write than necessary. On a higher level, they also prevent us from imagining the different ways the language could be extended. In this paper I show how to extend a dependently typed language with user-defined higher-order non-linear rewrite rules. Rewrite rules are a form of equality reflection that is applied automatically by the typechecker. I have implemented rewrite rules as an extension to Agda, and I give six examples how to use them both to make proofs easier and to experiment with extensions of type theory. I also show how to make rewrite rules interact well with other features of Agda such as η-equality, implicit arguments, data and record types, irrelevance, and universe level polymorphism. Thus rewrite rules break the chains on computation and put its power back into the hands of its rightful owner: yours.
Cite as

Jesper Cockx. Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 2:1-2:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cockx:LIPIcs.TYPES.2019.2,
  author =	{Cockx, Jesper},
  title =	{{Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{2:1--2:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.2},
  URN =		{urn:nbn:de:0030-drops-130666},
  doi =		{10.4230/LIPIcs.TYPES.2019.2},
  annote =	{Keywords: Dependent types, Proof assistants, Rewrite rules, Higher-order rewriting, Agda}
}
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