Skip to main content

Browse the archive

Raw File
meta.yml 
fullname: Monadic effects and equational reasoning in Coq
shortname: monae
organization: affeldt-aist
opam_name: coq-monae
community: false
action: true
coqdoc: false

synopsis: >-
  Monads and equational reasoning in Coq
description: |-
  This Coq library contains a hierarchy of monads with their laws used
  in several examples of monadic equational reasoning.
authors:
- name: Reynald Affeldt
  initial: true
- name: David Nowak
  initial: true
- name: Takafumi Saikawa
  initial: true
- name: Jacques Garrigue
  initial: false
- name: Celestine Sauvage
  initial: false
- name: Kazunari Tanaka
  initial: false

opam-file-maintainer: Reynald Affeldt <reynald.affeldt@aist.go.jp>

license:
  fullname: LGPL-2.1-or-later
  identifier: LGPL-2.1-or-later
  file: LICENSE

supported_coq_versions:
  text: Coq 8.13
  opam: '{ (>= "8.13" & < "8.14~") | (= "dev") }'

tested_coq_opam_versions:
- version: '1.12.0-coq-8.13'
  repo: 'mathcomp/mathcomp'

dependencies:
- opam:
    name: coq-mathcomp-ssreflect
    version: '{ (>= "1.12.0" & < "1.13~") }'
  description: |-
    [MathComp ssreflect](https://math-comp.github.io)
- opam:
    name: coq-mathcomp-fingroup
    version: '{ (>= "1.12.0" & < "1.13~") }'
  description: |-
    [MathComp fingroup](https://math-comp.github.io)
- opam:
    name: coq-mathcomp-algebra
    version: '{ (>= "1.12.0" & < "1.13~") }'
  description: |-
    [MathComp algebra](https://math-comp.github.io)
- opam:
    name: coq-mathcomp-solvable
    version: '{ (>= "1.12.0" & < "1.13~") }'
  description: |-
    [MathComp solvable](https://math-comp.github.io)
- opam:
    name: coq-mathcomp-field
    version: '{ (>= "1.12.0" & < "1.13~") }'
  description: |-
    [MathComp field](https://math-comp.github.io)
- opam:
    name: coq-mathcomp-analysis
    version: '{ (>= "0.3.6" & < "0.4~") }'
  description: |-
    [MathComp analysis](https://github.com/math-comp/analysis)
- opam:
    name: coq-infotheo
    version: '{ >= "0.3.2" & < "0.4~"}'
  description: |-
    [Infotheo](https://github.com/affeldt-aist/infotheo)
- opam:
    name: coq-paramcoq
    version: '{ >= "1.1.2" & < "1.2~" }'
  description: |-
    [Paramcoq](https://github.com/coq-community/paramcoq)

namespace: monae

keywords:
- name: monae
- name: effects
- name: probability
- name: nondeterminism

#date:
#- 2021-02-21

publications:
- pub_url: https://staff.aist.go.jp/reynald.affeldt/documents/monae.pdf
  pub_title: A hierarchy of monadic effects for program verification using equational reasoning
  pub_doi: 10.1007/978-3-030-33636-3_9
- pub_url: https://arxiv.org/abs/2003.09993
  pub_title: A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism
- pub_url: https://arxiv.org/abs/2011.03463
  pub_title: Extending Equational Monadic Reasoning with Monad Transformers

#make_target: [
#  [make "-j%{jobs}%"]
#  [make "sect5"]
#  [make "-C" "impredicative_set"]
#]
#
#install: [ [make "install_full"] ]

build: |-
  ## Building and installation instructions

  The easiest way to install the latest released version of Monadic effects and equational reasoning in Coq
  is via [OPAM](https://opam.ocaml.org/doc/Install.html):
  
  ```shell
  opam repo add coq-released https://coq.inria.fr/opam/released
  opam install coq-monae
  ```

  It installs two directories in `coq/user-contrib`: `monae` and
  `monaeImpredicativeSet`.

  To instead build and install manually (with GNU `make`), do:
  ``` shell
  git clone https://github.com/affeldt-aist/monae.git
  cd monae
  make -j 4
  make sect5
  make -C impredicative_set
  make install
  ```

documentation: |-
  ## Overview

  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] (from Sect. 5)
  - formalization of the geometrically convex monad (main reference:
    [Cheung, Distributive Interaction of Algebraic Effects, PhD Thesis, U. Oxford, 2017])

  ![Available monads](./hier.png "Available Monads")

  ## Files

  - [monae_lib.v](./monae_lib.v): simple additions to base libraries
  - [hierarchy.v](./hierarchy.v): hierarchy of monadic effects
  - [monad_lib.v](./monad_lib.v): basic lemmas about monads
  - [category.v](./category.v): formalization of categories (generalization of ~hierarchy.v~)
  - [fail_lib.v](./fail_lib.v): lemmas about fail monad and related monads
  - [state_lib.v](./state_lib.v): lemmas about state-related monads
  - [trace_lib.v](./trace_lib.v): lemmas about about the state-trace monad
  - [proba_lib.v](./proba_lib.v): about the probability monad
  - [monad_composition.v](./monad_composition.v): composing monads
  - [monad_transformer.v](./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](./monad_model.v): concrete models of monads (up to state and trace monads)
  - [proba_monad_model.v](./proba_monad_model.v): concrete model of the probability monad
  - [gcm_model.v](./gcm_model.v): model of the geometrically convex monad
  - [altprob_model.v](./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](./smallstep.v): semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs

  ## About Installation with Windows 10
 
  Installation of monae on Windows is less simple.
  First install infotheo following the [instructions for Windows 10](https://github.com/affeldt-aist/infotheo).
  Once infotheo is installed (with opam), do:
  - `opam install coq-monae` or `git clone git@github.com:affeldt-aist/monae.git; opam install .`

  ## Original License

  Before version 0.2, monae was distributed under the terms of the `GPL-3.0-or-later` license
back to top