Domain-aware session types

Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We develop a generalization of existing Curry-Howard interpretations of (binary) session types by relying on an extension of linear logic with features from hybrid logic, in particular modal worlds that indicate domains. These worlds govern domain migration, subject to a parametric accessibility relation familiar from the Kripke semantics of modal logic. The result is an expressive new typed process framework for domain-aware, message-passing concurrency. Its logical foundations ensure that well-typed processes enjoy session fidelity, global progress, and termination. Typing also ensures that processes only communicate with accessible domains and so respect the accessibility relation. Remarkably, our domain-aware framework can specify scenarios in which domain information is available only at runtime; flexible accessibility relations can be cleanly defined and statically enforced. As a specific application, we introduce domain-aware multiparty session types, in which global protocols can express arbitrarily nested sub-protocols via domain migration. We develop a precise analysis of these multiparty protocols by reduction to our binary domain-aware framework: complex domain-aware protocols can be reasoned about at the right level of abstraction, ensuring also the principled transfer of key correctness properties from the binary to the multiparty setting.

Original languageEnglish
Title of host publication30th International Conference on Concurrency Theory, CONCUR 2019
EditorsWan Fokkink, Rob van Glabbeek
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959771214
DOIs
Publication statusPublished - 1 Aug 2019
Event30th International Conference on Concurrency Theory, CONCUR 2019 - Amsterdam, Netherlands
Duration: 27 Aug 201930 Aug 2019

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume140
ISSN (Print)1868-8969

Conference

Conference30th International Conference on Concurrency Theory, CONCUR 2019
CountryNetherlands
CityAmsterdam
Period27/08/1930/08/19

Keywords

  • Hybrid Logic
  • Linear Logic
  • Process Calculi
  • Session Types

Fingerprint Dive into the research topics of 'Domain-aware session types'. Together they form a unique fingerprint.

Cite this