Interactive Analyzer

Parse a session type, build its state space, check lattice properties, and visualize the Hasse diagram.

Session type

Load benchmark

Analyzing…

Session Type Grammar Reference

S  ::=  &{ m₁ : S₁ , ... , mₙ : Sₙ }    -- branch (external choice)
     |  +{ l₁ : S₁ , ... , lₙ : Sₙ }    -- selection (internal choice)
     |  ( S₁ || S₂ )                    -- parallel
     |  rec X . S                        -- recursion
     |  X                                -- variable
     |  end                              -- terminated
     |  S₁ . S₂                          -- sequencing