WCTP2025 Talks

Verification for Program Manipulations using Iris

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

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.

On the other hand, in systems that perform static source code changes, such as macro and template metaprogramming, users can change the syntax without affecting the 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.

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. (to appear)

Abstract

Coverage checking is an essential static analysis for preventing runtime errors in languages with pattern matching. We present a work-in-progress formalization of Maranget’s algorithm in Agda. The algorithm handles simple patterns but does not support complex patterns such as those involving GADTs or pattern guards. We have formally proven the algorithm’s correctness and termination. Furthermore, our formalization is compatible with agda2hs, enabling extraction of a verified coverage checker implemented in Haskell. This work serves as a foundation for formalizing more efficient or expressive coverage checking algorithms.