Model composition methods that preserve logic proofs in software design
Dependently Typed Model Composition for Matching Logic
Logic in Computer Science
Summary
Sometimes when combining parts of a software system, it is tricky to ensure that the combined system still follows all the rules each part followed separately. The authors look at a way to combine these parts—called models—using a logical framework called matching logic. They make sure that if each part satisfies certain rules, then the combined model does too. Their work uses detailed type systems to make it easier to check these combinations automatically in computer proof tools.
What this means in practice
- •For formal methods engineers: Combine verified software modules ensuring that overall correctness proofs remain valid after integration.
- •For program verification developers: Support mechanized proofs of program behavior when building complex systems from smaller verified components.
A theory result. No direct application yet.
Authors
Ádám Kurucz, Péter Bereczky, Dániel Horpácsi
Abstract
This paper investigates model compositionâoften referred to as "gluing"âwithin the framework of matching logic. Specifically, we examine the systematic combination of existing signatures, variable valuations, theories, and their corresponding models. Our primary objective is to ensure that this composition preserves satisfaction proofs; that is, any theory validated by the individual constituent models is also validated by the resulting composite model. Our definitions are based on a polyadic, sorted variant of matching logic, which has also been expressed in the Rocq proof assistant. Therefore, we outline our definitions with dependent types for this work to serve as a direct blueprint for the mechanization in the short-term future.