Certifying data in multiparty session types
File(s)1-s2.0-S2352220816300864-main.pdf (566.4 KB)
Published version
Author(s)
Toninho, B
Yoshida, N
Type
Journal Article
Abstract
Multiparty session types (MPST) are a typing discipline for ensuring the coordination of multi-agent communication in concurrent and distributed programs. The original MPST framework mainly focuses on the communication aspects of concurrency, unable to capture important data invariants in communicating programs. This work introduces value dependent types to the MPST framework in order to increase its expressiveness for certifying invariants of data exchanged among multiple participants. The key idea is to impose constraints on the exchanged data, which is explicitly witnessed at runtime by proof objects. The enriched MPST framework provides programmers with a precise global description of the interaction and data dependent patterns, from which local (data dependent) descriptions can be automatically generated for each endpoint, faithfully capturing at a local level the global data constraints. The framework ensures the absence of communication errors and guarantees communication progress in well-typed multiparty sessions. We also develop an extension of value dependencies based on proof irrelevance that enables the selective erasure of proof objects at runtime.
Date Issued
2016-12-09
Date Acceptance
2016-12-09
Citation
Journal of Logical and Algebraic Methods in Programming, 2016, 90, pp.61-83
ISSN
2352-2208
Publisher
Elsevier
Start Page
61
End Page
83
Journal / Book Title
Journal of Logical and Algebraic Methods in Programming
Volume
90
Copyright Statement
© 2016 The Authors. Published by Elsevier Inc. This is an open access article under the CC
BY license (http://creativecommons.org/licenses/by/4.0/).
BY license (http://creativecommons.org/licenses/by/4.0/).
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Commission of the European Communities
Engineering & Physical Science Research Council (EPSRC)
Grant Number
ERI 025567 (EP/K034413/1)
PO 1553380
EP/K011715/1
612985
EP/N027833/1
Subjects
Science & Technology
Technology
Computer Science, Theory & Methods
Logic
Computer Science
Science & Technology - Other Topics
Session types
Multiparty session types
Value dependent types
Publication Status
Published