MobilityReadingGroup

Polymorphic Session Processes as Morphisms

Bernardo TONINHO, Nobuko YOSHIDA

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.

@inproceedings{TY2019,
  author = {Bernardo Toninho and Nobuko Yoshida},
  title = {{Polymorphic Session Processes as Morphisms}},
  booktitle = {The Art of Modelling Computational Systems: a Journey from Logic and Concurrency to Security and Privacy},
  pages = {101--117},
  publisher = {Springer},
  year = 2019
}

@inproceedings{TY2019,
  author = {Bernardo Toninho and Nobuko Yoshida},
  title = {{Polymorphic Session Processes as Morphisms}},
  booktitle = {The Art of Modelling Computational Systems: a Journey from Logic and Concurrency to Security and Privacy},
  pages = {101--117},
  publisher = {Springer},
  doi = "10.1007/978-3-030-31175-9_7",
  year = 2019
}