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.
The Art of Modelling Computational SystemsThe Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy
