The PCM library

The PCM library provides a formalisation of Partial Commutative Monoids (PCMs), a common algebraic structure used in separation logic for verification of pointer-manipulating sequential and concurrent programs.

The library provides lemmas for mechanised and automated reasoning about PCMs in the abstract, but also supports concrete common PCM instances, such as heaps, histories, and mutexes.

This library relies on propositional and functional extentionality axioms.

Meta

• Author(s):
  • Aleksandar Nanevski (initial)
  • Anton Trunov
  • Alexander Gryzlov
• License: Apache-2.0
• Compatible Rocq/Coq versions: 9.0 or later
• Additional dependencies:
  • MathComp ssreflect 2.4 or later
  • Hierarchy Builder 1.7.0 or later
  • MathComp algebra
• Rocq/Coq namespace: pcm
• Related publication(s): none

Building and installation instructions

The easiest way to install the latest released version of The PCM library is via OPAM:

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

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/imdea-software/fcsl-pcm.git
cd fcsl-pcm
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

Getting help

If you need assistance or would like to report a bug, drop us an email: fcsl@software.imdea.org or open an issue.

History and context

More information can be obtained via the FCSL web page.

An earlier version of this library was developed as a part of Hoare type theory, which is now rebased on FCSL-PCM. The original version of HTT can be found here.