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

Funding

Caires and Toninho are supported by NOVA LINCS (Ref. UID/CEC/04516/2019). Pérez is supported by the NWO VIDI Project No. 016.Vidi.189.046: "Unifying Correctness for Communicating Software". Pfenning is supported by NSF Grant No. CCF-1718267: "Enriching Session Types for Practical Concurrent Programming".

Cite As Get 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
    0
    Metadata Views

Related Versions

References

  1. Samson Abramsky. Computational Interpretations of Linear Logic. Theor. Comput. Sci., 111(1&2):3-57, 1993. URL: https://doi.org/10.1016/0304-3975(93)90181-R.
  2. Stephanie Balzer, Bernardo Toninho, and Frank Pfenning. Manifest Deadlock-Freedom for Shared Session Types. In Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, pages 611-639, 2019. Google Scholar
  3. Emmanuel Beffara. A Concurrent Model for Linear Logic. Electr. Notes Theor. Comput. Sci., 155:147-168, 2006. URL: https://doi.org/10.1016/j.entcs.2005.11.055.
  4. Gianluigi Bellin and Philip J. Scott. On the pi-Calculus and Linear Logic. Theor. Comput. Sci., 135(1):11-65, 1994. URL: https://doi.org/10.1016/0304-3975(94)00104-9.
  5. Torben Braüner and Valeria de Paiva. Intuitionistic Hybrid Logic. J. of App. Log., 4:231-255, 2006. Google Scholar
  6. Michele Bugliesi and Giuseppe Castagna. Behavioural typing for safe ambients. Comput. Lang., 28(1):61-99, 2002. URL: https://doi.org/10.1016/S0096-0551(02)00008-5.
  7. Luís Caires and Jorge A. Pérez. Multiparty Session Types Within a Canonical Binary Theory, and Beyond. In Formal Techniques for Distributed Objects, Components, and Systems - 36th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6-9, 2016, Proceedings, pages 74-95, 2016. Extended version with proofs at URL: https://sites.google.com/a/jorgeaperez.net/www/publications/medium16long.pdf.
  8. Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho. Behavioral Polymorphism and Parametricity in Session-Based Communication. In ESOP, volume 7792 of LNCS. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_19.
  9. Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho. Domain-Aware Session Types (Extended Version). CoRR, abs/1907.01318, 2019. URL: http://arxiv.org/abs/1907.01318.
  10. Luís Caires and Frank Pfenning. Session Types as Intuitionistic Linear Propositions. In CONCUR, volume 6269 of LNCS, pages 222-236. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_16.
  11. Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Mathematical Structures in Computer Science, 26(3):367-423, 2016. URL: https://doi.org/10.1017/S0960129514000218.
  12. Sara Capecchi, Ilaria Castellani, and Mariangiola Dezani-Ciancaglini. Information Flow Safety in Multiparty Sessions. In Bas Luttik and Frank Valencia, editors, EXPRESS, volume 64 of EPTCS, pages 16-30, 2011. URL: https://doi.org/10.4204/EPTCS.64.2.
  13. Sara Capecchi, Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Tamara Rezk. Session Types for Access and Information Flow Control. In CONCUR, volume 6269 of LNCS, pages 237-252. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_17.
  14. 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, August 23-26, 2016, Québec City, Canada, pages 33:1-33:15, 2016. Google Scholar
  15. Luca Cardelli, Giorgio Ghelli, and Andrew D. Gordon. Types for the Ambient Calculus. Inf. Comput., 177(2):160-194, 2002. URL: https://doi.org/10.1006/inco.2001.3121.
  16. Luca Cardelli and Andrew D. Gordon. Mobile ambients. Theor. Comput. Sci., 240(1):177-213, 2000. URL: https://doi.org/10.1016/S0304-3975(99)00231-5.
  17. Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Jorge A. Pérez. Self-adaptation and secure information flow in multiparty communications. Formal Asp. Comput., 28(4):669-696, 2016. URL: https://doi.org/10.1007/s00165-016-0381-3.
  18. Kaustuv Chaudhuri, Carlos Olarte, Elaine Pimentel, and Joëlle Despeyroux. Hybrid Linear Logic, revisited. Mathematical Structures in Computer Science, 2019. URL: https://hal.inria.fr/hal-01968154.
  19. Romain Demangeon and Kohei Honda. Nested Protocols in Session Types. In CONCUR 2012 - Concurrency Theory - 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, UK, September 4-7, 2012. Proceedings, pages 272-286, 2012. URL: https://doi.org/10.1007/978-3-642-32940-1_20.
  20. Romain Demangeon, Kohei Honda, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python. Formal Methods in System Design, 46(3):197-225, 2015. URL: https://doi.org/10.1007/s10703-014-0218-8.
  21. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types. In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, pages 174-186. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_18.
  22. Joëlle Despeyroux, Carlos Olarte, and Elaine Pimentel. Hybrid and Subexponential Linear Logics. Electr. Notes Theor. Comput. Sci., 332:95-111, 2017. Google Scholar
  23. 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, CSL 2012, September 3-6, 2012, Fontainebleau, France, pages 228-242, 2012. Google Scholar
  24. Mariangiola Dezani-Ciancaglini and Ugo de'Liguoro. Sessions and Session Types: An Overview. In WS-FM 2009, volume 6194 of LNCS, pages 1-28. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14458-5_1.
  25. Pablo Garralda, Adriana B. Compagnoni, and Mariangiola Dezani-Ciancaglini. BASS: boxed ambients with safe sessions. In Annalisa Bossi and Michael J. Maher, editors, PPDP, pages 61-72. ACM, 2006. URL: https://doi.org/10.1145/1140335.1140344.
  26. Simon J. Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Inf., 42(2-3):191-225, 2005. URL: https://doi.org/10.1007/s00236-005-0177-z.
  27. Jean-Yves Girard and Yves Lafont. Linear Logic and Lazy Computation. In TAPSOFT'87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, pages 52-66, 1987. URL: https://doi.org/10.1007/BFb0014972.
  28. Hannah Gommerstadt, Limin Jia, and Frank Pfenning. Session-Typed Concurrent Contracts. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, pages 771-798, 2018. Google Scholar
  29. Matthew Hennessy and James Riely. Resource Access Control in Systems of Mobile Agents. Inf. Comput., 173(1):82-120, 2002. URL: https://doi.org/10.1006/inco.2001.3089.
  30. Kohei Honda. Types for Dynamic Interaction. In CONCUR, volume 715 of LNCS, pages 509-523. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_35.
  31. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language Primitives and Type Discipline for Structured Communication-Based Programming. In ESOP'98, LNCS. Springer, 1998. URL: https://doi.org/10.1007/BFb0053567.
  32. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In George C. Necula and Philip Wadler, editors, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 273-284. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328472.
  33. Limin Jia, Hannah Gommerstadt, and Frank Pfenning. Monitors and blame assignment for higher-order session types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 582-594, 2016. Google Scholar
  34. Naoki Kobayashi. A New Type System for Deadlock-Free Processes. In CONCUR 2006 - Concurrency Theory, 17th International Conference, CONCUR 2006, Bonn, Germany, August 27-30, 2006, Proceedings, pages 233-247, 2006. Google Scholar
  35. Ugo Dal Lago and Paolo Di Giamberardino. Soft Session Types. In EXPRESS, volume 64 of EPTCS, pages 59-73, 2011. URL: https://doi.org/10.4204/EPTCS.64.5.
  36. Robin Milner, Joachim Parrow, and David Walker. A Calculus of Mobile Processes, part I/II. Inf. Comput., 100(1):1-77, 1992. Google Scholar
  37. Luca Padovani. Deadlock and lock freedom in the linear π-calculus. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 72:1-72:10, 2014. Google Scholar
  38. Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear Logical Relations for Session-Based Concurrency. In ESOP, volume 7211 of LNCS, pages 539-558. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28869-2_27.
  39. Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. Inf. Comput., 239:254-302, 2014. URL: https://doi.org/10.1016/j.ic.2014.08.001.
  40. Jason Reed. Hybridizing a Logical Framework. Electr. Notes Theor. Comput. Sci., 174(6):135-148, 2007. Google Scholar
  41. Davide Sangiorgi. pi-Calculus, Internal Mobility, and Agent-Passing Calculi. Theor. Comput. Sci., 167(1&2):235-274, 1996. URL: https://doi.org/10.1016/0304-3975(96)00075-8.
  42. Davide Sangiorgi and David Walker. The π-calculus: A Theory of Mobile Processes. Cambridge University Press, New York, NY, USA, 2001. Google Scholar
  43. Alex K. Simpson. The proof theory and semantics of intuitionistic modal logic. PhD thesis, University of Edinburgh, UK, 1994. URL: http://hdl.handle.net/1842/407.
  44. Bernardo Toninho, Luís Caires, and Frank Pfenning. Dependent session types via intuitionistic linear type theory. In Proc. of PPDP '11, pages 161-172, New York, NY, USA, 2011. ACM. URL: https://doi.org/10.1145/2003476.2003499.
  45. Bernardo Toninho, Luís Caires, and Frank Pfenning. Corecursion and Non-divergence in Session-Typed Processes. In Trustworthy Global Computing - 9th International Symposium, TGC 2014, Rome, Italy, September 5-6, 2014. Revised Selected Papers, pages 159-175, 2014. Google Scholar
  46. Bernardo Toninho and Nobuko Yoshida. Depending on Session-Typed Processes. In Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, pages 128-145, 2018. Google Scholar
  47. Philip Wadler. Propositions as sessions. J. Funct. Program., 24(2-3):384-418, 2014. URL: https://doi.org/10.1017/S095679681400001X.
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