[ICFP'22] Formal Reasoning about Layered Monadic Interpreters

Formal Reasoning about Layered Monadic Interpreters (Video, ICFP 2022)
Irene Yoon, Yannick Zakowski, and Steve Zdancewic
(University of Pennsylvania, USA; Inria, France; University of Pennsylvania, USA)

Abstract: Monadic computations built by interpreting, or handling, operations of a
free monad are a compelling formalism for modeling language semantics and
defining the behaviors of effectful systems.
The resulting layered semantics offer the promise of modular reasoning principles
based on the equational theory of the underlying monads.
However, there are a number of obstacles to using such layered
interpreters in practice. With more layers comes more boilerplate and glue
code needed to define the monads and interpreters involved. That overhead is
compounded by the need to define and justify the relational reasoning
principles that characterize the equivalences at each layer.

This paper addresses these problems by significantly extending the
capabilities of the Coq interaction trees (ITrees) library, which
supports layered monadic interpreters. We characterize a rich class of
interpretable monads---obtained by applying monad transformers to
ITrees---and show how to generically lift interpreters through them. We
also introduce a corresponding framework for relational reasoning about
'equivalence of monads up to a relation R'. This collection of
typeclasses, instances, new reasoning principles, and tactics greatly
generalizes the existing theory of the ITree library, eliminating large
amounts of unwieldy boilerplate code and dramatically simplifying proofs.

Video Tags: Coq, monads, coinduction, compiler correctness, icfp22main-p21-p, doi:10.1145/3547630, doi:10.5281/zenodo.6913915, orcid:0000-0003-3388-1257, orcid:0000-0003-4585-6470, orcid:0000-0002-3516-1512, Artifacts Available, Artifacts Evaluated , Reusable