The study of expressiveness of concurrent processes via session types
opens a connection between linear logic and mobile processes, grounded in the
rigorous logical background of propositions-as-types. One such study includes a
notion of parametric session polymorphism, which connects session typed processes
with rich higher-order functional computations. This work proposes a
novel and non-trivial application of session parametricity – an encoding of inductive
and coinductive session types, justified via the theory of initial algebras
and final co-algebras using a processes-as-morphisms viewpoint. The correctness
of the encoding (i.e. universality) relies crucially on parametricity and the associated
relational lifting of sessions.