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.6.0.tar.gz
sha256=4a31e6794c735d5e474ae94c4864635abcdc9daee576839871e2ffcd04ef484f

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:fcsl

Published: 20 Sep 2022

Dependencies

None

Dev Dependencies (2)

  1. coq-mathcomp-ssreflect (>= "1.13.0" & < "1.16~") | (= "dev")
  2. coq (>= "8.14" & < "8.17~") | (= "dev")

Used by (1)

  1. coq-htt = "1.1.0"

Conflicts

None