All formalizations of session types rely on linear types for soundness as
session-typed communication channels must change their type at every
operation. Embedded language implementations of session types follow
suit. They either rely on clever typing constructions to guarantee
linearity statically, or on run-time checks that approximate
linearity.

We present a new language-embedded implementation of session types,
which is inspired by the inversion-of-control design principle. With
our approach, all application programs are intrinsically session-typed and
unable to break linearity by construction. Our design relies on a tiny
encapsulated library, for which linearity remains a proof
obligation that can be discharged once and for all when the library is built.

We demonstrate that our proposed design extends to a wide range of
features of session type systems: branching, recursion, multichannel
and higher-order sessions, as well as context-free sessions. The
multichannel extension provides an embedded implementation of
session types which guarantees deadlock freedom by construction.

The development reported in this paper is fully backed by
type-checked Agda code.