Home

Awesome

<!--- This file was generated from `meta.yml`, please do not edit manually. Follow the instructions on https://github.com/coq-community/templates to regenerate. --->

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:

This library has been applied to other formalizations:

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:

Original License

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