README.org

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

** Requirements

• [[https://coq.inria.fr][Coq]] 8.9.0 or 8.9.1
• [[https://github.com/math-comp/math-comp][Mathematical Components library]] 1.8.0
• [[https://github.com/math-comp/analysis][MathComp-Analysis]] 0.2.0 which requires
  • [[https://github.com/math-comp/bigenough/][bigenough]] first release
  • [[https://github.com/math-comp/finmap][finmap]] 1.2.0
• [[https://github.com/affeldt-aist/infotheo][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