Subject: Ssreflect Users Discussion List
List archive
- From: Anton Trunov <>
- To:
- Subject: [ssreflect] FCSL-PCM release 1.0
- Date: Sun, 22 Apr 2018 10:32:45 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
- Ironport-phdr: 9a23:+0biXRWH1Xa+e8rhCn7vao6aViHV8LGtZVwlr6E/grcLSJyIuqrYbBWDt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XlsN+g61Urg+iqRJx3YDaZ5qYNOZnfqPYYd8aRXZNUthXWidcAo28dYwPD+8ZMOtEqYn9u1wOrR2jDgeyHuPv1zlIhnjo3aYn1OkuCwfG3BAnH9IIqnjbts/5NLsIUeCoyqnIyivDYuhZ2Tf48ofIcxQhreuQUrJ3dMrc0E8iHB7LgFWXrIzqJTKV1uIVvmia6upvSPyghHQ9pwF2uDivyd8giobIhoIJylDE6D52zJwpKt2/TU52Z8OvHphItyyCKYd6XscvT3trtSs60LEKpIC3cSsQxJg6xBPTdeSLfouV7h75SOqdOyl0iG9/dL6imhq+7U6twfDmWMauylZFtC9Fn8HMtn8T0xzT7dCKSv5n8Ueg3TaDzg7S6vtYLUwtm6rXNp0szqAqmpoctkTDGSD2mEHog6OMakok/e2o5/zmYrXguJCcK5d5hh/iPqkqgMCyAuQ1PhITU2SF+umwzqDv8E7nTLlSi/05iKjZsJTUJcQBoa65BhdY3Zwl6xajCDem1s4UkmMdIFJZYhKHko7pO1bQIP3jAve/hk6jkDZvx/zcIrLhBZDNImDZkLj9ZbZ991JcyA0rwNBE/JJUEK8OIPz3WkDvqNPYEgQ0Mxe0wubiENVyzJkSWWOJAq+DMaPdq0WE5uw1I7rEWIhAoy3nJvYh6vXypXoigxoce7Oo1N0Wbmq5F7JoORa3e33p1/4HDWAM9jYkUertlhXWWDhPYHD0VuQg/Cw9D5yOAoLKR4Tri7uEinToVqZKb3xLXwjfWUzjcJ+JDq9VOXCiZ/R5mzlBboCPDooo1BWgrgj/kuM1Ie/d+ylevpXmhoEsu7/j0Coq/DkxNPyzlnmXRjgtzGwNTj4ymqt4pB4lkwrR4e1Dm/VdUOdrybZJXwM9b8COyuV7D5XtQFqEcI7ZEhCpRdKpBTx3RdU0kYcD
Dear list,
It is our pleasure to announce the first release of the FCSL-PCM library!
FCSL-PCM is a part of Fine-grained Concurrent Separation Logic framework,
more information is
available at https://software.imdea.org/fcsl/
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.
It is based on the Coq proof assistant, SSReflect proof language, and
Mathcomp library.
The source code can be found at https://github.com/imdea-software/fcsl-pcm
The library is available on OPAM via coq-released repository.
Documentation and tutorials will be available this summer.
Happy hacking,
The FCSL-PCM team
- [ssreflect] FCSL-PCM release 1.0, Anton Trunov, 04/22/2018
Archive powered by MHonArc 2.6.18.