package coq-fcsl-pcm

  1. Overview
  2. No Docs
Partial Commutative Monoids

Install

Dune Dependency

software.imdea.org Edit opam file Versions (11)

Authors

  1. A
    Aleksandar Nanevski

Maintainers

  1. F
    FCSL <fcsl@software.imdea.org>

Sources

v1.3.0.tar.gz
sha256=3ac78341d681df1a35ad720a84b81089eec1bee30197b15d15b29a3d8c3cec85

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

Tags

keyword:separation logic keyword:partial commutative monoid category:Computer Science/Data Types and Data Structures logpath:fcsl date:2020-10-15

Published: 15 Oct 2020

Dependencies

None

Dev Dependencies (2)

  1. coq-mathcomp-ssreflect (>= "1.10.0" & < "1.12~") | (= "dev")
  2. coq (>= "8.11" & < "8.13~") | (= "dev")

Used by

None

Conflicts

None