← All papers
Complete Heyting Algebra Semantics for an Intuitionistic Version of Matching Logic (Extended Abstract)
cs.LO
Sep 28, 2026 · v1
TL;DR
The soundness proof of the proposed intuitionistic matching logic proof system was formalized in Lean, largely with Claude Opus via Claude Code.
Abstract
We present work in progress towards an intuitionistic version of Applicative Matching Logic. We introduce a semantics based on complete Heyting algebras, and propose a proof system which we prove to be sound relative to this semantics.
Problem
Applicative Matching Logic is classical. An intuitionistic version needs a suitable semantics and a proof system that is sound with respect to it.
Approach
The authors define a semantics for an intuitionistic Applicative Matching Logic based on complete Heyting algebras and propose a proof system for it. The soundness proof was formalized in Lean alongside development of the theory. The formalization was produced mostly autonomously by Claude Opus models in Claude Code, with interactive feedback from the authors.
Results
The proof system is proved sound relative to the complete Heyting algebra semantics, with a Lean formalization of the proof. The formalization process helped rule out early unsound or degenerate versions of the system.