DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2019.39

Domain-Aware Session Types

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

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{caires_et_al:LIPIcs.CONCUR.2019.39,
  author =	{Caires, Lu{\'\i}s and P\'{e}rez, Jorge A. and Pfenning, Frank and Toninho, Bernardo},
  title =	{{Domain-Aware Session Types}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{39:1--39:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.39},
  URN =		{urn:nbn:de:0030-drops-109417},
  doi =		{10.4230/LIPIcs.CONCUR.2019.39},
  annote =	{Keywords: Session Types, Linear Logic, Process Calculi, Hybrid Logic}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2016.16

Composing Interfering Abstract Protocols

Authors: Filipe Militão, Jonathan Aldrich, and Luís Caires

Published in: LIPIcs, Volume 56, 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract

The undisciplined use of shared mutable state can be a source of program errors when aliases unsafely interfere with each other. While protocol-based techniques to reason about interference abound, they do not address two practical concerns: the decidability of protocol composition and its integration with protocol abstraction. We show that our composition procedure is decidable and that it ensures safe interference even when composing abstract protocols. To evaluate the expressiveness of our protocol framework for safe shared memory interference, we show how this same protocol framework can be used to model safe, typeful message-passing concurrency idioms.

Cite as

Filipe Militão, Jonathan Aldrich, and Luís Caires. Composing Interfering Abstract Protocols. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 16:1-16:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{militao_et_al:LIPIcs.ECOOP.2016.16,
  author =	{Milit\~{a}o, Filipe and Aldrich, Jonathan and Caires, Lu{\'\i}s},
  title =	{{Composing Interfering Abstract Protocols}},
  booktitle =	{30th European Conference on Object-Oriented Programming (ECOOP 2016)},
  pages =	{16:1--16:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-014-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{56},
  editor =	{Krishnamurthi, Shriram and Lerner, Benjamin S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2016.16},
  URN =		{urn:nbn:de:0030-drops-61108},
  doi =		{10.4230/LIPIcs.ECOOP.2016.16},
  annote =	{Keywords: shared memory interference, protocol composition, aliasing, linearity}
}

Document

DOI: 10.4230/LIPIcs.CSL.2012.228

Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication

Authors: Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract

Prior work has shown that intuitionistic linear logic can be seen as a session-type discipline for the pi-calculus, where cut reduction in the sequent calculus corresponds to synchronous process reduction. In this paper, we exhibit a new process assignment from the asynchronous, polyadic pi-calculus to exactly the same proof rules. Proof-theoretically, the difference between these interpretations can be understood through permutations of inference rules that preserve observational equivalence of closed processes in the synchronous case. We also show that, under this new asynchronous interpretation, cut reductions correspond to a natural asynchronous buffered session semantics, where each session is allocated a separate communication buffer.

Cite as

Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho. Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 228-242, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{deyoung_et_al:LIPIcs.CSL.2012.228,
  author =	{DeYoung, Henry and Caires, Lu{\'\i}s and Pfenning, Frank and Toninho, Bernardo},
  title =	{{Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{228--242},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.228},
  URN =		{urn:nbn:de:0030-drops-36753},
  doi =		{10.4230/LIPIcs.CSL.2012.228},
  annote =	{Keywords: linear logic, cut reduction, asynchronous pi-calculus, session types}
}

Search Results

Documents authored by Caires, Luís

Domain-Aware Session Types

Abstract

Cite as

Composing Interfering Abstract Protocols

Abstract

Cite as

Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication

Abstract

Cite as

Thanks for your feedback!

Could not send message