meta.yml

fullname: The PCM library
shortname: fcsl-pcm
organization: imdea-software
opam_name: coq-fcsl-pcm
community: false
action: true
coqdoc: false

synopsis: >-
  Coq library of Partial Commutative Monoids
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.
authors:
- name: Aleksandar Nanevski
  initial: true
- name: Anton Trunov
  initial: false
- name: Alexander Gryzlov
  initial: false

maintainers:
- name: Alexander Gryzlov
  nickname: clayrat

opam-file-maintainer: fcsl@software.imdea.org

opam-file-version: dev

license:
  fullname: Apache-2.0
  identifier: Apache-2.0
  file: LICENSE

supported_coq_versions:
  text: Coq 8.19 to 8.20
  opam: '{ (>= "8.19" & < "8.21~") | (= "dev") }'

tested_coq_opam_versions:
- version: '2.2.0-coq-8.19'
  repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.20'
  repo: 'mathcomp/mathcomp'
- version: 'latest-coq-dev'
  repo: 'mathcomp/mathcomp'

dependencies:
- opam:
    name: coq-mathcomp-ssreflect
    version: '{ (>= "2.2.0" & < "2.3~") | (= "dev") }'
  description: |-
    [MathComp ssreflect 2.2](https://math-comp.github.io)
- opam:
    name: coq-mathcomp-algebra
  description: |-
    [MathComp algebra](https://math-comp.github.io)

namespace: pcm

keywords:
- name: partial commutative monoids
- name: separation logic
- name: concurrency

categories:
- name: Computer Science/Data Types and Data Structures

documentation: |-
  ## Getting help

  If you need assistance or would like to report a bug, drop us an email:
  <fcsl@software.imdea.org> or open an [issue](https://github.com/imdea-software/fcsl-pcm/issues).

  ## History and context

  More information can be obtained via the [FCSL web page](https://software.imdea.org/fcsl/).

  An earlier version of this library was developed as a part of [Hoare type
  theory](https://github.com/imdea-software/htt), which is now rebased on FCSL-PCM. The original
  version of HTT can be found [here](https://software.imdea.org/~aleks/htt/).