title | lang | header-includes | |
---|---|---|---|
Monadic effects and equational reasoning in Coq |
en |
|
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.
The current stable release of Monadic effects and equational reasoning in Coq can be downloaded from GitHub.
Related publications, if any, are listed below.
- A hierarchy of monadic effects for program verification using equational reasoning doi:10.1007/978-3-030-33636-3_9
- A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism
- Extending Equational Monadic Reasoning with Monad Transformers doi:10.4230/LIPIcs.TYPES.2020.2
- Report issues on GitHub
- Reynald Affeldt
- David Nowak
- Takafumi Saikawa
- Jacques Garrigue
- Celestine Sauvage
- Kazunari Tanaka