Write a choreography on the left: one program describing how several roles interact. It is projected into one process per role, shown in the tabs on the right, each with its local session type. Edit a process and the choreography follows, if the processes still form one.
The badge well-typed ⇒ deadlock-free means that the choreography on the left has a global type. Two results of the paper's Lean development make that a guarantee about the processes:
well-typed ⇒ deadlock-free
ChorProgTyping.projectPool
ChorProgTyping.deadlock_freedom
Type checking, projection and reverse projection are the Lean development's own functions, compiled to WebAssembly and run in your browser; nothing is sent to a server. Type inference returns a typing derivation, so a program it accepts is well-typed.
Each tab is type-checked on its own, but that does not rule out deadlocks: the roles must agree on one global type. So edited processes earn the badge only through reverse projection, which searches for a choreography whose projection is exactly the edited tabs (ProcProgFamily.unproject_sound) and which must itself be well-typed. If there is none, the problems list says where the roles disagree, and the choreography on the left stays as it is. If the reconstruction projects to the same processes as the left side, the left text is kept; otherwise it is replaced.
ProcProgFamily.unproject_sound
In an editor, Tab indents; press Esc first to move focus out with Tab. In the role tabs, the arrow keys, Home and End switch roles. A location in the problems list jumps to the error.