Document Open Access Logo

Multiparty Session Types as Coherence Proofs

Authors Marco Carbone, Fabrizio Montesi, Carsten Schürmann, Nobuko Yoshida

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2015.412.pdf
  • Filesize: 0.61 MB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • Programming languages
  • Type systems
  • Session Types
  • Linear Logic

Metrics

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

Abstract

We propose a Curry-Howard correspondence between a language for programming multiparty sessions and a generalisation of Classical Linear Logic (CLL). In this framework, propositions correspond to the local behaviour of a participant in a multiparty session type, proofs to processes, and proof normalisation to executing communications. Our key contribution is generalising duality, from CLL, to a new notion of n-ary compatibility, called coherence. Building on coherence as a principle of compositionality, we generalise the cut rule of CLL to a new rule for composing many processes communicating in a multiparty session. We prove the soundness of our model by showing the admissibility of our new rule, which entails deadlock-freedom via our correspondence.

Cite As Get BibTex

Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. Multiparty Session Types as Coherence Proofs. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 412-426, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CONCUR.2015.412

Author Details

Marco Carbone
Fabrizio Montesi
Carsten Schürmann
Nobuko Yoshida

References

  1. Samson Abramsky, Simon J. Gay, and Rajagopal Nagarajan. Interaction categories and the foundations of typed concurrent programming. In NATO ASI DPD, pages 35-113, 1996. Google Scholar
  2. Gianluigi Bellin and Philip J. Scott. On the pi-calculus and linear logic. Theor. Comput. Sci., 135(1):11-65, 1994. Google Scholar
  3. 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
  4. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In CONCUR, pages 222-236, 2010. Google Scholar
  5. Marco Carbone and Søren Debois. A graphical approach to progress for structured communication in web services. In Proc. of ICE'10, 2010. Google Scholar
  6. Marco Carbone and Fabrizio Montesi. Deadlock-freedom-by-design: multiparty asynchronous global programming. In POPL, pages 263-274, 2013. Google Scholar
  7. Marco Carbone, Fabrizio Montesi, and Carsten Schürmann. Choreographies, logically. In CONCUR, pages 47-62, 2014. Google Scholar
  8. Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, and Luca Padovani. On global types and multi-party session. LMCS, 8(1), 2012. Google Scholar
  9. Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. Global progress for dynamically interleaved multiparty sessions. MSCS, 760:1-65, 2015. Google Scholar
  10. Romain Demangeon and Kohei Honda. Nested protocols in session types. In CONCUR, pages 272-286, 2012. Google Scholar
  11. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In ICALP (2), pages 174-186, 2013. Google Scholar
  12. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. Google Scholar
  13. 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
  14. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Proc. of POPL, volume 43(1), pages 273-284. ACM, 2008. Google Scholar
  15. Julien Lange and Emilio Tuosto. Synthesising choreographies from local session types. In CONCUR, pages 225-239, 2012. Google Scholar
  16. Julien Lange, Emilio Tuosto, and Nobuko Yoshida. From communicating machines to graphical choreographies. In POPL 2015, pages 221-232. ACM, 2015. Google Scholar
  17. Sam Lindley and J. Garrett Morris. A semantics for propositions as sessions. In ESOP, pages 560-584, 2015. Google Scholar
  18. Fabrizio Montesi and Nobuko Yoshida. Compositional choreographies. In CONCUR, pages 425-439, 2013. Google Scholar
  19. Luca Padovani, Vasco Thudichum Vasconcelos, and Hugo Torres Vieira. Typing liveness in multiparty communicating systems. In COORDINATION, pages 147-162, 2014. Google Scholar
  20. D. Sangiorgi and D. Walker. The π-calculus: a Theory of Mobile Processes. Cambridge University Press, 2001. Google Scholar
  21. Scribble project home page. URL: http://www.scribble.org.
  22. Vasco T. Vasconcelos. Fundamentals of session types. Inf. Comput., 217:52-70, 2012. Google Scholar
  23. Philip Wadler. Propositions as sessions. In 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact