Monadic equational reasoning in Coq

This repository contains a formalization of monads including several models, examples of monadic equational reasoning, and an application to program semantics.

Formalized papers:

• [Gibbons and Hinze, Just do It: Simple Monadic Equational Reasoning, ICFP 2011] (except Sect. 10.2)
• [Gibbons, Unifying Theories of Programming with Monads, UTP 2012] (up to Sect. 7.2)
• [Mu, Functional Pearls: Reasoning and Derivation of Monadic Programs, A case study of non-determinism and state, 2017] (up to Sect. 5)
• [Jones and Duponcheel, Composing Monads, Yale RR 1993] (Sections 2 and 3)

Other reference:

• [Cheung, Distributive Interaction of Algebraic Effects, PhD Thesis, U. Oxford, 2017]

Files

• monad.v: basics of monadic equational reasoning
• state_monad.v: about the state monad
• trace_monad.v: about the state-trace monad
• proba_monad.v: about the probability monad
• monad_composition.v: composing monads
• model.v: definition common to *_model.v files
• monad_model.v: concrete models of monads (corresponding to {,state_,trace_}monad.v)
• proba_monad_model.v: concrete model of the probability monad
• altprob_model.v: model of combined choice
• example_spark.v: example of Spark aggregation
• example_nqueens.v: example of the n-queens puzzle
• example_relabeling.v: example of tree relabeling
• example_monty.v: examples of Monty Hall problem
• smallstep.v: semantics for an imperative language
• smallstep_monad.v: equivalence operational semantics/denotation
• smallstep_examples.v: sample imperative programs

Requirements

• Coq 8.9.0 or 8.9.1
• Mathematical Components library 1.8.0
• MathComp-Analysis 0.2.0 which requires
  • bigenough first release
  • finmap 1.2.0
• infotheo github master version

All versions (except infotheo) available from opam.

Compiles also with mathcomp 1.9.0, analysis 0.2.2, finmap 1.2.1 (using the mathcomp-1.9.0 branch of infotheo).

Installation

1. make
   • rm Makefile.coq beforehand in case of Coq upgrade