From session π to coincident event structures

This webpage is an implementation of a translation from session π to coincident event structure. It takes as input a session π term and draws the event structure corresponding to its interpretation.

Accepted syntax

The syntax follows that of the paper, with some adjustements:

P ::=
   (nu a b c ...) (P)                                     { restriction }
|  a?INPUT-NAMES. P | a?INPUT-NAMES                       { input without label }
|  a?label INPUT-NAMES. P | a?label INPUT-NAMES           { input with one branch with label }
|  a?{label1: NAMES: P; label2: NAMES: P; ... }           { branching input }
|  a!OUTPUT-NAMES                                         { output without label }
|  a!label OUTPUT-NAMES                                   { output/selection }
|  P | Q                                                  { parallel composition }
|  P + Q                                                  { nondeterministic sum }
INPUT-NAMES ::=
              { empty list }
| (x, ..., z) { list of names }

OUTPUT-NAMES ::=
              { empty list }
| [x, ..., z] { list of names }
    

The coname of a name x is denoted x'.

Type inference

Before computing the interpretation, the session types of each channel is inferred, as types are necessary to compute the interpretation (necessary when interpreting a channel output).
Be careful about conames: if you want to represent communication on a channel a, you need to need to use a on one side, and a' on the other. (See the examples for more details).

Translation

Conflict is drawn as a blue dotted line; otherwise the same convention as in the paper apply.