Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper introduces a framework for compositional program verification using polynomial functors in dependent type theory, where functors represent program interfaces, Kleisli morphisms are implementations, and dependent polynomials encode specifications. Implementations and their verifications are shown to compose via wiring diagrams, leveraging a compositional coalgebraic operational semantics based on Mealy machines. The authors formalize the underlying categorical structure in Agda, suggesting potential generalizations to concurrency and relational verification.
Compositional program verification, notoriously difficult, gets a boost from polynomial functors and dependent type theory, offering a path to more modular and scalable verification techniques.
We present a framework for compositional program verification based on polynomial functors in dependent type theory. In this framework, polynomial functors serve as program interfaces, Kleisli morphisms for the free monad monad serve as implementations, and dependent polynomials encode pre/postcondition specifications. We show that implementations and their verifications compose via wiring diagrams, and that Mealy machines provide a compositional coalgebraic operational semantics. We identify the abstract categorical structure underlying this compositionality as a monoidal functor from specifications to interfaces with a compatible monoidal natural transformation of lax monoidal presheaves; this opens the door to generalizations to other categories, monoidal products, etc., including settings for concurrency and relational verification, which we sketch. As a proof-of-concept, the entire framework has been formalized in Agda.