package coq-fcsl-pcm

  1. Overview
  2. No Docs
Coq library of Partial Commutative Monoids

Install

Dune Dependency

github.com Edit opam file Versions (11)

Authors

  1. A
    Aleksandar Nanevski
  2. A
    Anton Trunov
  3. A
    Alexander Gryzlov

Maintainers

  1. F
    fcsl@software.imdea.org

Sources

v1.8.0.tar.gz
sha256=8dfa84d19445c7f45cc62df731812795098a79b285ff5572f9205a84a07b387f

Description

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.

Tags

category:Computer Science/Data Types and Data Structures keyword:partial commutative monoids keyword:separation logic keyword:concurrency logpath:pcm

Published: 14 May 2023

Dependencies (2)

  1. coq-mathcomp-algebra
  2. coq-mathcomp-ssreflect >= "1.15.0" & < "1.20~"

Dev Dependencies (1)

  1. coq (>= "8.15" & < "8.21~") | (= "dev")

Used by (3)

  1. coq-disel >= "2.3"
  2. coq-disel-examples >= "2.3"
  3. coq-htt = "1.3.0"

Conflicts

None