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.

翻译：我们提出一个基于依赖类型理论中多项式函子的组合式程序验证框架。在该框架中，多项式函子充当程序接口，自由单子单子的Kleisli态射充当实现，而依赖多项式编码前后置条件规约。我们证明实现及其验证可通过接线图进行组合，并且Mealy机提供组合余代数操作语义。我们将这种组合性背后的抽象范畴结构识别为从规约到接口的幺半函子，并伴随一个松幺半预层的相容幺半自然变换；这为此类结构向其他范畴、幺半积等的推广打开了大门，包括我们简要勾勒的并发与关系验证设置。作为概念验证，整个框架已在Agda中形式化。