Disel Versions Save

• fixed deprecations
• use Dune as build system in Coq library opam packages
• depends on htt 1.2.0 or later and fcsl-pcm 1.7.0 or later
• compatible with MathComp 1.13.0, 1.14.0, 1.15.0, and Coq 8.14, 8.15, 8.16

• fixed deprecations
• works with latest Coq (8.12.0) and mathcomp-ssreflect (1.11.0)

• fixed more deprecations and better adhere to build best practices
• works with latest Coq (8.9.0) and mathcomp-ssreflect (1.7.0)
• maintenance release suitable for use in other projects

• fixed deprecation warnings
• works with latest Coq (8.8.1) and mathcomp-ssreflect (1.7.0)
• relies on fcsl-pcm library for heap theory
• maintenance release suitable for use in other projects

Disel v1.5

The artifact, as accepted to appear POPL 2018, with the accompanying paper Programming and Proving with Distributed Protocols by Ilya Sergey, James R. Wilcox, and Zachary Tatlock.

Features

• Higher-order dependent type theory for verifying distributed systems;
• Elaboration of protocol invariants;
• Horizontal composition of protocols in specifications;

Changes since v.1.0

• Added support for send-hooks to compose protocols with dependencies;

First release, created in order to generate an OPAM package.