---
# This file was generated from `meta.yml`, please do not edit manually.
# Follow the instructions on https://github.com/coq-community/templates to regenerate.
title: Monadic effects and equational reasoning in Coq
lang: en
header-includes:
  - |
    <style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>
    <style type="text/css"> h1 {margin-left: 0em; padding: 0px; text-align: center} </style>
    <style type="text/css"> h2 {margin-left: 0em; padding: 0px; color: #580909} </style>
    <style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>
    <style type="text/css"> body { width: 1100px; margin-left: 30px; }</style>
---

<div style="text-align:left"><img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px">
<a href="https://github.com/affeldt-aist/monae">View the project on GitHub</a>
<img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px"></div>

## About

Welcome to the Monadic effects and equational reasoning in Coq project website!

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

This is an open source project, licensed under the LGPL-2.1-or-later.

## Get the code

The current stable release of Monadic effects and equational reasoning in Coq can be [downloaded from GitHub](https://github.com/affeldt-aist/monae/releases).

## Documentation


Related publications, if any, are listed below.

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

## Help and contact

- Report issues on [GitHub](https://github.com/affeldt-aist/monae/issues)

## Authors and contributors

- Reynald Affeldt
- David Nowak
- Takafumi Saikawa
- Jacques Garrigue
- Celestine Sauvage
- Kazunari Tanaka