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.7.0.tar.gz
sha256=e4e2da2ba6a82ce16562a6ddca5fae34d68c053978b9fdbbea8ade883a163e84

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: 11 Nov 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 (3)

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

Conflicts

None