Isabelle/Nonuniform sessions
Code
Examples
Formalization