Characteristic formulae for session types

Lange, Julien and Yoshida, Nobuko (2016) Characteristic formulae for session types. In: TACAS 2016, 2-8 April 2016, Eindhoven, The Netherlands. (doi:https://doi.org/10.1007/978-3-662-49674-9_52) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided. (Contact us about this Publication)
Official URL
http://dx.doi.org/10.1007/978-3-662-49674-9_52

Abstract

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.

Item Type: Conference or workshop item (Proceeding)
Divisions: Faculties > Sciences > School of Computing
Depositing User: Julien Lange
Date Deposited: 12 Jul 2017 14:54 UTC
Last Modified: 25 Aug 2017 15:03 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/62253 (The current URI for this page, for reference purposes)
Lange, Julien: https://orcid.org/0000-0001-9697-1378
  • Depositors only (login required):