Formalization of Coverage Checking in Agda

DOI

10.2991/978-94-6239-638-8_4How to use a DOI?

Keywords

formal verification; pattern match; coverage check; agda

Abstract

Coverage checking is an essential static analysis for preventing runtime errors in programming languages with pattern matching. We present a work-in-progress formalization of Maranget’s algorithm in Agda. Although the algorithm targets simple patterns and does not support complex patterns such as those involving GADTs or pattern guards, it remains practical since most programs only use simple patterns. We prove correctness and termination of the algorithm. Furthermore, we structure the formalization to be compatible with agda2hs, enabling extraction of a verified coverage checker in Haskell. This work provides a foundation for mechanizing more efficient or more powerful coverage checking algorithms.

Copyright

© 2026 The Author(s)

Open Access

Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 4.0 International License (http://creativecommons.org/licenses/by-nc/4.0/), which permits any noncommercial use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

Download article (PDF)

TY  - CONF
AU  - Satoshi Takimoto
AU  - Sosuke Moriguchi
AU  - Takuo Watanabe
PY  - 2026
DA  - 2026/04/30
TI  - Formalization of Coverage Checking in Agda
BT  - Proceedings of the  Workshop on Computation: Theory and Practice (WCTP 2025)
PB  - Atlantis Press
SP  - 33
EP  - 49
SN  - 2589-4900
UR  - https://doi.org/10.2991/978-94-6239-638-8_4
DO  - 10.2991/978-94-6239-638-8_4
ID  - Takimoto2026
ER  -