This repository contains a proof that two formulations of equivalence for
session types coincide: One direct coinductive variant (Equiv.v) and one
based on bisimilarity of trace languages (TL.v) or extensional equality of
the trace language sets (TLSets.v). The main result is in
TraceBisimEquiv.v. Additionally, a proof that direct equivalence is, in fact,
an equivalence can be found in EquivFacts.v
We make use of two custom axioms in the definition of trace languages to get
around Coq's productivity checker. They appear in TL.v, where you may also
find a justification of their use. Otherwise, we only use well-known classical
axioms (and only in the parts of the codebase concerned with classical sets,
i.e. TLSets.v).
Building requires that coqc version 8.5 is on the path. (Unfortunately, this
development does not compile with version 8.6 or higher yet because we are
blocked on the TLC library.)
git submodule init
git submodule update
cd lib/tlc/
env SERIOUS=1 make -j5 # for vo output; 5 is the number of concurrent jobs
# make -j5 # for vio output
cd ../..
./configure
make -j5 # for vo output
# make -j5 quick # for vio output
# make J=5 vio2vo # for turning vio output into vo output
(Sorry that this is not more automated, but I can't for the life of mine
figure out the incantation that makes coq_makefile behave sensibly.)
If you use CoqIDE or Proof General, make sure they honor the settings from
_CoqProject (generated by ./configure).
Your use of this software is governed by the MIT license, a copy of which may be found in the LICENSE file.
This repository also contains a modified copy of Arthur Charguéraud's TLC library, licensed under the CeCILL-B license.