Formal Reasoning About Layered Monadic Interpreters

Our paper extends the Coq Interaction Trees library to support elegant reasoning about layered monadic interpreters. This artifact contains the corresponding formalism, and the case study of an Imp2Asm compiler.


This documentation includes pretty-printed Coq source, which can also be found as .v files in the git repository. The pretty-printed html hides proof scripts by default, so you can click on Show Proofs at the top of the page to display all proofs.

Proof Structure

This artifact builds on top of the Interaction Tree library, and this artifact includes the original ITree library along with the relevant extension which is the contribution of the paper. The Coq contribution of this artifact is outlined in these following files. N.B. There are other files included in the table of contents and the artifact submission which are part of the original ITree library.

Paper Correspondence

Below is a table that shows how the definition of laws and their instances correspond to the Coq mechanization. /
Coq Proof
Item Description Subitems File Name
Section 3.1, 3.2
Building Layered Monadic Interpreters
Trigger Subevent.v Class Trigger
Class Subevent
Subevent Instances
Section Subevent_Instances
Section 3.4
Interpretable monads
Interp Interp.v Class Interp
HFunctor.v Class HFunctor
InterpFacts.v Instance stack_interp
Figure 7
Well-formedness Laws of EqmR
EqmRMonad.v Class EqmR_OK
Section 4.2
Image of a Monadic Computation
EqmRMonad.v Definition mayRet
Figure 8
EqmRMonad Laws
EqmRMonad.v Class EqmRMonadLaws
Figure 9
EqmRMonadInverses Laws
EqmRMonad.v Class EqmRMonadInversionProperties
Section 4.1-4.3
ID Monad Instance for EqmR
Section 4.1-4.3
State Monad Instance for EqmR Laws
Section 4.1-4.3
State Monad Instance for EqmR Laws
Section 4.1-4.3
Error Monad Instance for EqmR Laws
Section 4.1-4.3
ITree Monad Instance for EqmR Laws (strong bisimulation)
Leaves ITree_strong.v Returns
Section 4.1-4.3
ITree Monad Instance for EqmR Laws (weak bisimulation)
Leaves ITree_weak.v Returns
Section 4.1-4.3
Prop Monad Instance for EqmR Laws
Figure 10
Monad morphism laws
EqmRMonadT.v Section MonadMorphism
Figure 11*
Monad transformer well-formedness conditions
EqmRMonadT.v Class MonadTLaws
Section 4.4
StateT Monad Transformer Law Instance
Section 4.4
ErrorT Monad Transformer Law Instance
Section 4.5
Relating Computation across Distinct Monads
Figure 12
Interpretation laws
Figure 13
Higher-order functor laws
Figure 14
Composable Structures and Laws
MonadT Laws EqmRMonadT.v compose_MonadT
IterativeMonadT Laws
HFunctor.v compose_HFunctor
HFunctor Laws
* N.B. : The MonadMorphism laws is parameterized over a monad morphism from monad M to monad MT, while the MonadTLaws is parameterized over a monad transformer. Figure 11 is not explicitly stated as a typeclass but is proved for the state and error transformers (in stateT and errorT).

Case Study

The case study in Section 6 is in tutorial/, where the definition of languages are in Imp.v and Asm.v, and the proof of correctness for the compiler is in Imp2AsmCorrectness.v. The commuted version of this proof mentioned in Section 6.2.3 is in tutorial_commute/. The custom tactics mentioned is in tutorial/Proofmode.v.

Typeclass dependencies

Proof dependency structure Typeclass dependency in EqmR Framework is shown above. The red nodes are the category theory-relevant typeclasses from the Interaction Trees library (most notably the theory of iterative monads and equivalence on Kleisli arrows), the yellow nodes are standard functional programming typeclasses (functor, monad, monad transformers, higher-order functors), and the green nodes represent the structural properties that we have formalized in the framework. A dotted line connects an "operational" typeclass to its corresponding laws, and solid arrows represent dependencies.