Compositional Program Verification with Polynomial Functors in Dependent Type Theory

C. B. Aberlé

We present a framework for compositional program verification based on polynomial functors in dependent type theory. In this framework, polynomial functors serve as program interfa…