Document Open Access Logo

Domain-Aware Session Types

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



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.39.pdf
  • Filesize: 0.61 MB
  • 17 pages

Document Identifiers

Author Details

Luís Caires
  • Universidade Nova de Lisboa, Portugal
Jorge A. Pérez
  • University of Groningen, The Netherlands
Frank Pfenning
  • Carnegie Mellon University, Pittsburgh, PA, USA
Bernardo Toninho
  • Universidade Nova de Lisboa, Portugal

Cite AsGet BibTex

Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho. Domain-Aware Session Types. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 39:1-39:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.39

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
  • Theory of computation → Type structures
  • Software and its engineering → Message passing
Keywords
  • Session Types
  • Linear Logic
  • Process Calculi
  • Hybrid Logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail