This was sort of news to me:
Our new MPST theory is a case of behavioural type system: it treats types as
simple processes that reduce and evolve along a typed computation; and since types are simpler
than programs, they can be analysed with simpler methods (e.g., finite model checking via our
parameter φ, cf. ğ6).
found via https://lobste.rs/t/formalmethods
cc @tgrospic @leithaus