MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Polymorphic Session Processes as Morphisms
Bernardo TONINHO, Nobuko YOSHIDA
To appear in
The Art of Modelling Computational Systems: a Journey from Logic and Concurrency to Security and Privacy (FC)

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 = {1--17},
  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 = {1--17},
  year = 2019
}