Document Open Access Logo

A Universal Session Type for Untyped Asynchronous Communication

Authors Stephanie Balzer, Frank Pfenning, Bernardo Toninho

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2018.30.pdf
  • Filesize: 0.64 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
  • Theory of computation → Linear logic
Keywords
  • Session types
  • sharing
  • pi-calculus
  • bisimulation

Metrics

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

Abstract

In the simply-typed lambda-calculus we can recover the full range of expressiveness of the untyped lambda-calculus solely by adding a single recursive type U = U -> U. In contrast, in the session-typed pi-calculus, recursion alone is insufficient to recover the untyped pi-calculus, primarily due to linearity: each channel just has two unique endpoints. In this paper, we show that shared channels with a corresponding sharing semantics (based on the language SILL_S developed in prior work) are enough to embed the untyped asynchronous pi-calculus via a universal shared session type U_S. We show that our encoding of the asynchronous pi-calculus satisfies operational correspondence and preserves observable actions (i.e., processes are weakly bisimilar to their encoding). Moreover, we clarify the expressiveness of SILL_S by developing an operationally correct encoding of SILL_S in the asynchronous pi-calculus.

Cite As Get BibTex

Stephanie Balzer, Frank Pfenning, and Bernardo Toninho. A Universal Session Type for Untyped Asynchronous Communication. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CONCUR.2018.30

Author Details

Stephanie Balzer
  • Carnegie Mellon University, USA
Frank Pfenning
  • Carnegie Mellon University, USA
Bernardo Toninho
  • NOVA LINCS, Universidade Nova de Lisboa, Portugal

Funding

  • Balzer, Stephanie: NSF Grant No. CCF-1718267: "Enriching Session Types for Practical Concurrent Programming"
  • Pfenning, Frank: NSF Grant No. CCF-1718267: "Enriching Session Types for Practical Concurrent Programming"
  • Toninho, Bernardo: NOVA LINCS (Ref. UID/CEC/04516/2013)

References

  1. Robert Atkey. Observed communication semantics for classical processes. In European Symposium on Programming (ESOP), pages 56-82, 2017. Google Scholar
  2. Robert Atkey, Sam Lindley, and J. Garrett Morris. Conflation confers concurrency. In S. Lindley et al., editor, Wadler Festschrift, pages 32-55. Springer LNCS 9600, 2016. Google Scholar
  3. Stephanie Balzer and Frank Pfenning. Manifest sharing with session types. Proceedings of the ACM on Programming Languages (PACMPL), 1(ICFP):37:1-37:29, 2017. Google Scholar
  4. Stephanie Balzer and Frank Pfenning. Manifest sharing with session types. Technical Report CMU-CS-17-106, Carnegie Mellon University, March 2017. Google Scholar
  5. Romain Beauxis, Catuscia Palamidessi, and Frank D. Valencia. On the asynchronous nature of the asynchronous π-calculus. In Concurrency, Graphs and Models, volume 5065 of Lecture Notes in Computer Science, pages 473-492. Springer, 2008. Google Scholar
  6. P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and models. In 8th International Workshop on Computer Science Logic (CSL), volume 933 of Lecture Notes in Computer Science, pages 121-135. Springer, 1994. An extended version appeared as Technical Report UCAM-CL-TR-352, University of Cambridge. Google Scholar
  7. Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho. Behavioral polymorphism and parametricity in session-based communication. In European Symposium on Programming (ESOP), pages 330-349. Springer, 2013. Google Scholar
  8. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In 21st International Conference on Concurrency Theory (CONCUR), pages 222-236. Springer, 2010. Google Scholar
  9. Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Mathematical Structures in Computer Science, 26(3):367-423, 2016. Google Scholar
  10. Iliano Cervesato and Andre Scedrov. Relating state-based and process-based concurrency through linear logic. Information and Computation, 207(10):1044-1077, 2009. Google Scholar
  11. Karl Crary, Robert Harper, and Sidd Puri. What is a recursive module? In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 50-63, 1999. Google Scholar
  12. Ornela Dardha and Simon J. Gay. A new linear logic for deadlock-free session-typed processes. In Foundations of Software Science and Computation Structures (FoSSaCS), pages 91-109, 2018. Google Scholar
  13. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. In Principles and Practice of Declarative Programming (PPDP), pages 139-150, 2012. Google Scholar
  14. Ornela Dardha and Jorge A. Pérez. Comparing deadlock-free session typed processes. In EXPRESS/SOS, pages 1-15, 2015. Google Scholar
  15. Yuxin Deng, Robert J. Simmons, and Iliano Cervesato. Relating reasoning methodologies in linear logic and process algebra. Mathematical Structure in Computer Science, 26(5):868-906, 2016. Google Scholar
  16. Simon J. Gay and Malcolm Hole. Subtyping for session types in the π-calculus. Acta Informatica, 42(2-3):191-225, 2005. Google Scholar
  17. Hannah Gommerstadt, Limin Jia, and Frank Pfenning. Session-typed concurrent contracts. In A. Ahmed, editor, European Symposium on Programming (ESOP'18), pages 771-798, Thessaloniki, Greece, 2018. Springer LNCS 10801. Google Scholar
  18. Daniele Gorla. Towards a unified approach to encodability and separation results for process calculi. Information and Computation, 208(9):1031-1053, 2010. Google Scholar
  19. Dennis Griffith and Frank Pfenning. SILL. https://github.com/ISANobody/sill, 2015.
  20. Kohei Honda. Types for dyadic interaction. In 4th International Conference on Concurrency Theory (CONCUR), pages 509-523. Springer, 1993. Google Scholar
  21. Kohei Honda and Mario Tokoro. An object calculus for asynchronous communication. In 5th European Conference on Object-Oriented Programming (ECOOP), Lecture Notes in Computer Science, pages 133-147. Springer, 1991. Google Scholar
  22. Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In 7th European Symposium on Programming (ESOP), pages 122-138. Springer, 1998. Google Scholar
  23. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 273-284. ACM, 2008. Google Scholar
  24. Limin Jia, Hannah Gommerstadt, and Frank Pfenning. Monitors and blame assignment for higher-order session types. In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 582-594, 2016. Google Scholar
  25. Naoki Kobayashi. A type system for lock-free processes. Inf. Comput., 177(2):122-159, 2002. Google Scholar
  26. Naoki Kobayashi. A new type system for deadlock-free processes. In International Conference on Concurrency Theory (CONCUR), pages 233-247, 2006. Google Scholar
  27. Dimitrios Kouzapas and Nobuko Yoshida. Globally governed session semantics. Logical Methods in Computer Science, 10(4), 2014. Google Scholar
  28. Sam Lindley and J. Garrett Morris. A semantics for propositions as sessions. In European Symposium On Programming (ESOP), pages 560-584, 2015. Google Scholar
  29. Sam Lindley and J. Garrett Morris. Talking bananas: structural recursion for session types. In International Colloquium on Functional Progrmaming (ICFP), pages 434-447, 2016. Google Scholar
  30. Robin Milner. Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, 1999. Google Scholar
  31. Uwe Nestmann. What is a "good" encoding of guarded choice? Inf. Comput., 156(1-2):287-319, 2000. Google Scholar
  32. Luca Padovani. Deadlock and lock freedom in the linear π-calculus. In Computer Science Logic - Logic in Computer Science (CSL-LICS), pages 72:1-72:10, 2014. Google Scholar
  33. Catuscia Palamidessi. Comparing the expressive power of the synchronous and asynchronous pi-calculi. Mathematical Structures in Computer Science, 13(5):685-719, 2003. Google Scholar
  34. Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. Information and Computation, 239:254-302, 2014. Google Scholar
  35. Frank Pfenning and Dennis Griffith. Polarized substructural session types. In 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), pages 3-22. Springer, 2015. Google Scholar
  36. Jason Reed. A judgmental deconstruction of modal logic. Unpublished manuscript, January 2009. URL: http://www.cs.cmu.edu/~jcreed/papers/jdml.pdf.
  37. Davide Sangiorgi and David Walker. The π-Calculus - A Theory of Mobile Processes. Cambridge University Press, 2001. Google Scholar
  38. Bernardo Toninho. A Logical Foundation for Session-based Concurrent Computation. PhD thesis, Carnegie Mellon University and New University of Lisbon, 2015. Google Scholar
  39. Bernardo Toninho, Luís Caires, and Frank Pfenning. Functions as session-typed processes. In 15th International Conference on Foundations of Software Science and Computational Structures (FOSSACS), pages 346-360. Springer, 2012. Google Scholar
  40. Bernardo Toninho, Luís Caires, and Frank Pfenning. Higher-order processes, functions, and sessions: a monadic integration. In 22nd European Symposium on Programming (ESOP), pages 350-369. Springer, 2013. Google Scholar
  41. Bernardo Toninho and Nobuko Yoshida. On polymorphic sessions and functions - A tale of two (fully abstract) encodings. In European Symposium On Programming (ESOP), pages 827-855, 2018. Google Scholar
  42. Philip Wadler. Propositions as sessions. In 17th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 273-286. ACM, 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