coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] FCSL-PCM release 1.0

From: Anton Trunov <anton.a.trunov AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] FCSL-PCM release 1.0
Date: Fri, 20 Apr 2018 17:24:57 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=anton.a.trunov AT gmail.com; spf=Pass smtp.mailfrom=anton.a.trunov AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f175.google.com
Ironport-phdr: 9a23:EP01DBJjXkBWRZUgN9mcpTZWNBhigK39O0sv0rFitYgeKvvxwZ3uMQTl6Ol3ixeRBMOHs6kC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwtFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhicbODA2/27Zl89+gqxFrhymvBF/35fUYISJOPp+Yq/RY9UXTndBUMZLUCxBB5uxYpcJD+odOuZYqZT2qUUUrRujAwmsA/3vwSJPi3Ds2606z+MhEQfc0AM6Bd4OrG7UrMjzNKcVT+C416bIzTDZYPNX3Tfx8pTHchckofyVW797bMTfyU4qFwzfj1WQr5ToPzKQ1usQrWeU9fBsVeW1i24osw1xrTmvxtssionUnY0Z0EzL9SJ8wIszONa2S1Z7bMa6HJdMsyyWLYh7T8M4T211pio3yacKtYO5cSUK0Jgr2hrSZvKdf4SV7R/uVvydLSpkiH9nYr6yiBe//E69wePmTMa0ykxFri9dn9nMqH8N0xvT59CCSvRn/0eh3S+D1g7J6u1YOEw0m7fXJpwhz7IqmZoTtkPDHiDymErolqOZakIk+u2w5+TmZLXpuIOcOpdqhg3iNqkigM+yDOQiPgQTQWSW+v6w2KDh8ED5WLlKi+c5kqjdsJDUP8Qboau5DhdP3YYl9xa/CDGm3M4CknUdMFJFYg+Hj47uO1HQO/34AvK/jE6tkDdv3fzJIrrhApDVInjZjLjhZap961JbyAcr0d9f4ItUBqgdL/L3R0/+r8fVDgQ5Mgyx2+boEs9x1oIYWWKVA6+WKrnesVGS5rFnH+7Zb4gM/T35NvIN5vj0jHZ/l0VOU7Ou2M4+bmy/GLxaOVifZmSk1t4HDWAM+AN4UPb3jlqceTFWbne2Gak742doW8qdEY7fS9X10/S61yChE8gOPzEUOhW3CX7tMr68dbIJYSOWLNVml2VdB7ekQo4lkxqpsV2jkuY1Hq/v4iQd8Knb+p1t/eSKzEM98DV1C4KW1GTfFzgpzFNNfCc/2eVEmWI4ylqH1vIm0flRFNgW+OkRFwljasOawOt9BNT/HAnGe4XRRQ==

Dear Coq-Clubbers,

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

[Coq-Club] FCSL-PCM release 1.0, Anton Trunov, 04/20/2018