This repository contains a formalization of monads including examples of monadic equational reasoning and several models (in particular, a model for a monad that mixes non-deterministic choice and probabilistic choice). This corresponds roughly to the formalization of the following 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, Equational Reasoning for Non-determinism Monad: A Case study of Spark Aggregation, TR-IIS-19-002, Academia Sinica]
• [Mu, Calculating a Backtracking Algorithm: An exercise in Monadic Program Derivation, TR-IIS-29-003, Academia Sinica]
• [Mu, Functional Pearls: Reasoning and Derivation of Monadic Programs, A case study of non-determinism and state, 2017]
  • This is a draft paper. In the first release, we formalized this draft up to Sect. 5. The contents have been since superseded by [mu2019tr2] and [mu2019tr3].

This library has been applied to other formalizations:

• application to program semantics (see file smallstep.v)
• formalization of monad composition [Jones and Duponcheel, Composing Monads, Yale RR 1993] (Sections 2 and 3)
• formalization of monad transformers [Jaskelioff, Modular Monad Transformers, ESOP 2009] (up to Sect. 4)
  • completed with details from [Jaskelioff, Lifting of Operations in Modular Monadic Semantics, PhD 2009]
  • see directory impredicative_set for the formalization of [Jaskelioff, Modular Monad Transformers, ESOP 2009] up to Sect. 5
• formalization of the geometrically convex monad (main reference: [Cheung, Distributive Interaction of Algebraic Effects, PhD Thesis, U. Oxford, 2017])

• monae_lib.v: simple additions to base libraries
• hierarchy.v: hierarchy of monadic effects
• monad_lib.v: basic lemmas about monads
• category.v: formalization of categories (generalization of hierarchy.v)
• fail_lib.v: lemmas about fail monad and related monads
• state_lib.v: lemmas about state-related monads
• trace_lib.v: lemmas about about the state-trace monad
• proba_lib.v: about the probability monad
• monad_composition.v: composing monads
• monad_transformer.v: monad transformers
  • completed by ifmt_lifting.v and iparametricty_codensity.v in the directory impredicative_set
    • the directory impredicative_set contains a lighter version of Monae where monads live in Set and that compiles with impredicate-set
• monad_model.v: concrete models of monads (up to state and trace monads)
• proba_monad_model.v: concrete model of the probability monad
• gcm_model.v: model of the geometrically convex monad
• altprob_model.v: model of a monad that mixes non-deterministic choice and probabilistic choice
• example_*.v: various examples (Spark aggregation, the n-queens puzzle, tree relabeling, Monty Hall problem, monad transformers, etc.)
• smallstep.v: semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs

The preferred way to install monae is with opam because it takes care of the dependencies with other libraries. If not already done, add the repository for Coq libraries to opam and update:

1. opam repo add coq-released https://coq.inria.fr/opam/released
2. opam update

Version 0.2:

1. opam install coq-monae

• Coq 8.11 or 8.12
• Mathematical Components library 1.11.0
• infotheo 0.2
  • which requires MathComp-Analysis 0.3.2
    • which requires
      • finmap 1.5.0

All versions available from opam.

With Coq 8.11 or 8.12 and the last stable release of infotheo (the impredicative_set directory (as well as `make sect5`) require ParamCoq).

1. git clone [email protected]:affeldt-aist/monae.git
2. cd monae

If opam is installed, do:

1. opam install .

opam takes care of the dependencies.

If opam is not installed but if the requirements are met, do:

1. make
2. make install

Installation of monae on Windows is less simple. First install infotheo following the instructions for Windows 10. Once infotheo is installed:

1. If opam is available, do
   • opam install coq-monae or git clone [email protected]:affeldt-aist/monae.git; opam install .
2. If opam is not available (i.e., installation of MathComp using unzip, untar, cd, make, make install), do:
   • git clone [email protected]:affeldt-aist/monae.git
   • coq_makefile -o Makefile -f _CoqProject
   • make

LGPL-2.1-or-later

(Before version 0.2, monae was distributed under the terms of the GPL-3.0-or-later license.)

• MPC 2019 paper
• A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism (arXiv 2020)