WCTP2025 Talks

Formalization of Coverage Checking in Agda

Satoshi Takimoto, Sosuke Moriguchi & Takuo Watanabe
14th Workshop on Computation: Theory and Practice (WCTP 2025), Chotose, Dec. 1-3, 2025.

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.

Publication

Satoshi Takimoto, Sosuke Moriguchi, Takuo Watanabe, Formalization of Coverage Checking in Agda, in Proceedings of the Workshop on Computation: Theory and Practice (WCTP 2025), Atlantis Highlights in Computer Sciences, Vol. 24, pp. 33-49, Atlantis Press, Apr., 2026, DOI: 10.2991/978-94-6239-638-8_4 (open access)

Verification for Program Manipulations using Iris

Sosuke Moriguchi
14th Workshop on Computation: Theory and Practice (WCTP 2025), Chotose, Dec. 1-3, 2025.

Abstract

In this paper, we implement a framework for verifying programs targeting source code using the theorem prover Rocq and the program logic library Iris. As programming languages become more complex, it is becoming difficult to accurately describe their semantics. As a result, it is becoming increasingly difficult to predict the semantic issues that will arise when language extensions are added. In systems that perform static source code changes, such as macro and template metaprogramming, users can change syntax without affecting semantics. The proposed framework performs data-source mapping in the verification system, similar to metaprogramming, to extract another program from the data during program execution and verify its semantics. This paper verifies that the proposed method enables program verification of this kind.

Publication

Sosuke Moriguchi, Verification for Program Manipulations using Iris, in Proceedings of the Workshop on Computation: Theory and Practice (WCTP 2025), Atlantis Highlights in Computer Sciences, Vol. 24, pp. 7-16, Atlantis Press, Apr., 2026, DOI: 10.2991/978-94-6239-638-8_2 (open access)