index.md

title	lang	header-includes
Monadic effects and equational reasoning in Coq	en	<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>

View the project on GitHub

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.

Documentation

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

Help and contact

• Report issues on GitHub

Authors and contributors

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