Freer Equational Reasoning for Distributed and Probabilistic Systems

This work started as a rewrite/extension of FreeSpec Core using monae / ssreflect.

This work has been accepted for presentation to COMPAS26 (no paper available online).

Meta

• Author(s):
  • Hugo Forraz (initial)
• License: MIT License
• Additional dependencies:
  • MathComp
  • MathComp Analysis
  • MathComp Algebra Tactics
  • Monae
• Related publication(s):

Building and installation instructions

The easiest way to install the latest released version of Freer Equational Reasoning for Distributed and Probabilistic Systems is via OPAM:

opam repo add rocq-released https://rocq-prover.org/opam/released
opam install coq-FreerDPS

To instead build and install manually, you need to make sure that all the libraries this development depends on are installed. The easiest way to do that is still to rely on opam:

git clone https://github.com/FreerDPS/FreerDPS.git
cd FreerDPS
opam repo add rocq-released https://rocq-prover.org/opam/released
opam install --deps-only .
make   # or make -j <number-of-cores-on-your-machine>
make install