coq-fcsl-pcm

Partial Commutative Monoids 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 extensionality axioms: propositional and functional extentionality.

opam install coq-fcsl-pcm.1.0.0
homepage
http://software.imdea.org/fcsl/
license
Apache 2.0
bugs tracker
https://github.com/imdea-software/fcsl-pcm/issues
dependencies
coq (>= 8.7 & < 8.9~) & coq-mathcomp-ssreflect (>= 1.6.2 & < 1.8~)
source
https://github.com/imdea-software/fcsl-pcm/archive/v1.0.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.1.0.0