Document Open Access Logo

Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types

Authors Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, Philip Wadler

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.33.pdf
  • Filesize: 0.55 MB
  • 15 pages

Document Identifiers

Author Details

Marco Carbone
Sam Lindley
Fabrizio Montesi
Carsten Schürmann
Philip Wadler

Cite As Get BibTex

Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler. Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 33:1-33:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CONCUR.2016.33

Abstract

Wadler introduced Classical Processes (CP), a calculus based on a propositions-as-types correspondence between propositions of classical linear logic and session types. Carbone et al. introduced Multiparty Classical Processes, a calculus that generalises CP to multiparty session types, by replacing the duality of classical linear logic (relating two types) with a more general notion of coherence (relating an arbitrary number of types). This paper introduces variants of CP and MCP, plus a new intermediate calculus of Globally-governed Classical Processes (GCP). We show a tight relation between these three calculi, giving semantics-preserving translations from GCP to CP and from MCP to GCP. The translation from GCP to CP interprets a coherence proof as an arbiter process that mediates communications in a session, while MCP adds annotations that permit processes to communicate directly without centralised control.

Subject Classification

Keywords
  • Multiparty Session Types
  • Linear Logic
  • Propositions as Types

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Samson Abramsky. Proofs as processes. Theor. Comput. Sci., 135(1):5-9, 1994. Google Scholar
  2. Andi Bejleri and Nobuko Yoshida. Synchronous multiparty session types. ENTCS, 241:3-33, 2009. Google Scholar
  3. Gianluigi Bellin and Philip J. Scott. On the pi-calculus and linear logic. TCS, 135(1):11-65, 1994. Google Scholar
  4. Luís Caires and Jorge Perez. Multiparty session types within a canonical binary theory, and beyond. In FORTE, 2016. Google Scholar
  5. Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho. Behavioral polymorphism and parametricity in session-based communication. In ESOP, pages 330-349, 2013. Google Scholar
  6. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In CONCUR, pages 222-236, 2010. Google Scholar
  7. Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. MSCS, 26(3):367-423, 2016. Google Scholar
  8. Marco Carbone, Fabrizio Montesi, and Carsten Schürmann. Choreographies, logically. In CONCUR, pages 47-62, 2014. Google Scholar
  9. Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. Multiparty session types as coherence proofs. In CONCUR, pages 412-426, 2015. Google Scholar
  10. Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. Global progress for dynamically interleaved multiparty sessions. MSCS, 760:1-65, 2015. Google Scholar
  11. Kohei Honda, Vasco Vasconcelos, and Makoto Kubo. Language primitives and type disciplines for structured communication-based programming. In ESOP, pages 22-138, 1998. Google Scholar
  12. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. JACM, 63(1):9, 2016. Also: POPL, 2008, pages 273-284. Google Scholar
  13. Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. TCS, 410(46):4747-4768, 2009. Google Scholar
  14. Sam Lindley and Garrett Morris. Talking bananas: structural recursion for session types. In ICFP. ACM, 2016. To appear. Google Scholar
  15. Fabrizio Montesi and Nobuko Yoshida. Compositional choreographies. In CONCUR, pages 425-439, 2013. Google Scholar
  16. Jennifer Paykin and Steve Zdancewic. Linear λμ is CP (more or less). In A List of Successes That Can Change The World, pages 273-291, 2016. Google Scholar
  17. Frank Pfenning and Dennis Griffith. Polarized substructural session types. In Foundations of Software Science and Computation Structures, pages 3-22. Springer, 2015. Google Scholar
  18. Davide Sangiorgi. Pi-calculus, internal mobility, and agent-passing calculi. TCS, 167(1&2):235-274, 1996. Google Scholar
  19. A. S. Troelstra and H. Schwichtenberg. Basic Proof Theory (2nd Ed.). Cambridge University Press, 2000. Google Scholar
  20. Vasco T. Vasconcelos. Fundamentals of session types. Inf. Comput., 217:52-70, 2012. Google Scholar
  21. Philip Wadler. Propositions as sessions. In ICFP, pages 273-286, 2012. Google Scholar
  22. Philip Wadler. Propositions as sessions. JFP, 24(2-3):384-418, 2014. Also: ICFP, pages 273-286, 2012. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact