Verifying Effectful Haskell Programs in Coq

We show how various Haskell language features that are related to ambient effects can be modeled in Coq. For this purpose we build on previous work that demonstrates how to reason about existing Haskell programs by translating them into monadic Coq programs. A model of Haskell programs in Coq that is polymorphic over an arbitrary monad results in non-strictly positive types when transforming recursive data types likes lists. Such non-strictly positive types are not accepted by Coq’s termination checker. Therefore, instead of a model that is generic over any monad, the approach we build on uses a specific monad instance, namely the free monad in combination with containers, to model various kinds of effects. This model allows effect-generic proofs.