Certifying data in multiparty session types

Bernardo Toninho, Nobuko Yoshida

Research output: Contribution to journalArticle

8 Citations (Scopus)

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.

Original languageEnglish
Pages (from-to)61-83
Number of pages23
JournalJournal of Logical and Algebraic Methods in Programming
Volume90
DOIs
Publication statusPublished - Aug 2017

Keywords

  • Multiparty session types
  • Session types
  • Value dependent types

Fingerprint Dive into the research topics of 'Certifying data in multiparty session types'. Together they form a unique fingerprint.

Cite this