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

v2.0.0.tar.gz
sha256=ef2828c682217b7340834bcec4a2b245d2bea93cddb56dbc54efbc877680a96c

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: 18 Sep 2024

Dev Dependencies (2)

  1. coq-mathcomp-ssreflect (>= "2.2.0" & < "2.4~") | (= "dev")
  2. coq (>= "8.19" & < "8.21~") | (= "dev")

Used by (4)

  1. coq-disel >= "2.3"
  2. coq-disel-examples >= "2.3"
  3. coq-htt >= "2.0.0"
  4. coq-htt-core

Conflicts

None