An Extensible Approach to Session Polymorphism

Coq Implementation

The system from An Extensible Approach to Session Polymorphism has been implemented in Coq.

The document Guide to Coq Formalization describes the specific Coq encoding.

Coq has been used to verify the subject reduction, runtime safety, and conformance results in the paper.

Additionally, the examples from the paper have been typechecked with the Coq implementation:

• A "sink" process that consumes all of its input.
• A unidirectional forwarder that forwards messages from one channel to another.
• A bidirectional forwarder that forwards messages bidirectionally between two channels.
• A model of the Alternating-Bit Protocol that uses a lossy process to nondeterministically discard data.

The individual Coq source files can be browsed online. Alternatively, a ZIP archive of the Coq source (150Kb) and a ZIP archive of Coq source with compiled vernac objects (13Mb) can be downloaded.

To recompile the Coq source, run ./compile.sh from the release directory created when extracting the archive.

The Coq scripts have been verified with Coq version 8.3 (December 2010).