MobilityReadingGroup

Characteristic Formulae for Session Types

Julien LANGE, Nobuko YOSHIDA

Subtyping is a crucial ingredient of session type theory and its applications, notably to programming language implementations. In this paper, we study effective ways to check whether a session type is a subtype of another by applying a characteristic formulae approach to the problem.

Our core contribution is an algorithm to generate a modal μ-calculus formula that characterises all the supertypes (or subtypes) of a given type.

Subtyping checks can then be off-loaded to model checkers, thus incidentally yielding an efficient algorithm to check safety of session types, soundly and completely.

We have implemented our theory and compared its cost with other classical subtyping algorithms.

@inproceedings{LY2016,
  author = {Julien Lange and Nobuko Yoshida},
  title = {{Characteristic Formulae for Session Types}},
  booktitle = {22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  series = {LNCS},
  volume = {9636},
  pages = {833--850},
  publisher = {Springer},
  year = 2016
}

@inproceedings{LY2016,
  author = {Julien Lange and Nobuko Yoshida},
  title = {{Characteristic Formulae for Session Types}},
  booktitle = {22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  series = {LNCS},
  volume = {9636},
  pages = {833--850},
  publisher = {Springer},
  doi = "10.1007/978-3-662-49674-9_52",
  year = 2016
}