Type-system combining type-states and typed effects?

Has anyone succeeded in implementing or designing a type-system that combines both type-state (linear types) and effect types (e.g. Koka)?

• Kitten has some linear typing (still being figured out) as well as an effect system based on Koka’s. – Jon Purdy Jun 21 '16 at 1:07

A lot of work on types for $\pi$-calculus does this. See e.g. (1) for a unified system. Sequential languages can be embedded into $\pi$-calculus, so this work also applies to sequential languages.