Skip to content

affeldt-aist/monae

Folders and files

NameName
Last commit message
Last commit date

Latest commit

cb8cf79 · Jan 3, 2025
Dec 20, 2024
Dec 20, 2024
Jan 3, 2025
Jan 3, 2025
Jul 28, 2021
Jan 8, 2021
Oct 31, 2020
Apr 21, 2022
Oct 25, 2024
Jul 12, 2024
Jan 3, 2025
Dec 20, 2024
Dec 15, 2020
Dec 15, 2020
Jul 10, 2024
Jun 25, 2021
Jan 3, 2025

Repository files navigation

Monadic effects and equational reasoning in Coq

Docker CI

This Coq library contains a hierarchy of monads with their laws used in several examples of monadic equational reasoning.

Meta

Building and installation instructions

The easiest way to install the latest released version of Monadic effects and equational reasoning in Coq is via OPAM:

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:

git clone https://github.com/affeldt-aist/monae.git
cd monae
make -j 4
make install

Overview

This repository contains a formalization of monads including examples of monadic equational reasoning and several models. This includes for example 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].
  • [Mu and Chiang, Deriving Monadic Quicksort (Declarative Pearl), 2020]

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

Files

About Installation with Windows 11

Installation of monae on Windows is less simple. First install infotheo following the instructions for Windows 11. Once infotheo is installed (with opam), do:

  • opam install coq-monae or git clone [email protected]: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