Lange, Julien, Yoshida, Nobuko (2016) Characteristic formulae for session types. In: Chechik, M. and Raskin, J.F., eds. Lecture Notes in Computer Science. Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2016. 9636. pp. 833-850. Springer ISBN 978-3-662-49673-2. (doi: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) (KAR id:62253)
| 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. | |
| 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) |
|---|---|
| DOI/Identification number: | 10.1007/978-3-662-49674-9_52 |
| Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
| Depositing User: | Julien Lange |
| Date Deposited: | 12 Jul 2017 14:54 UTC |
| Last Modified: | 17 Aug 2022 12:22 UTC |
| Resource URI: | https://kar.kent.ac.uk/id/eprint/62253 (The current URI for this page, for reference purposes) |
University of Kent Author Information
Lange, Julien.
| Creator's ORCID: |
 https://orcid.org/0000-0001-9697-1378
|
|---|---|
| CReDIT Contributor Roles: |
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):
Altmetric
Altmetric
