A Universal Session Type for Untyped Asynchronous Communication
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.
Session types
sharing
pi-calculus
bisimulation
Theory of computation~Process calculi
Theory of computation~Linear logic
30:1-30:18
Regular Paper
Stephanie
Balzer
Stephanie Balzer
Carnegie Mellon University, USA
NSF Grant No. CCF-1718267: "Enriching Session Types for Practical Concurrent Programming"
Frank
Pfenning
Frank Pfenning
Carnegie Mellon University, USA
NSF Grant No. CCF-1718267: "Enriching Session Types for Practical Concurrent Programming"
Bernardo
Toninho
Bernardo Toninho
NOVA LINCS, Universidade Nova de Lisboa, Portugal
NOVA LINCS (Ref. UID/CEC/04516/2013)
10.4230/LIPIcs.CONCUR.2018.30
Robert Atkey. Observed communication semantics for classical processes. In European Symposium on Programming (ESOP), pages 56-82, 2017.
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.
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.
Stephanie Balzer and Frank Pfenning. Manifest sharing with session types. Technical Report CMU-CS-17-106, Carnegie Mellon University, March 2017.
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.
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.
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.
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.
Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Mathematical Structures in Computer Science, 26(3):367-423, 2016.
Iliano Cervesato and Andre Scedrov. Relating state-based and process-based concurrency through linear logic. Information and Computation, 207(10):1044-1077, 2009.
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.
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.
Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. In Principles and Practice of Declarative Programming (PPDP), pages 139-150, 2012.
Ornela Dardha and Jorge A. Pérez. Comparing deadlock-free session typed processes. In EXPRESS/SOS, pages 1-15, 2015.
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.
Simon J. Gay and Malcolm Hole. Subtyping for session types in the π-calculus. Acta Informatica, 42(2-3):191-225, 2005.
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.
Daniele Gorla. Towards a unified approach to encodability and separation results for process calculi. Information and Computation, 208(9):1031-1053, 2010.
Dennis Griffith and Frank Pfenning. SILL. https://github.com/ISANobody/sill, 2015.
https://github.com/ISANobody/sill
Kohei Honda. Types for dyadic interaction. In 4th International Conference on Concurrency Theory (CONCUR), pages 509-523. Springer, 1993.
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.
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.
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.
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.
Naoki Kobayashi. A type system for lock-free processes. Inf. Comput., 177(2):122-159, 2002.
Naoki Kobayashi. A new type system for deadlock-free processes. In International Conference on Concurrency Theory (CONCUR), pages 233-247, 2006.
Dimitrios Kouzapas and Nobuko Yoshida. Globally governed session semantics. Logical Methods in Computer Science, 10(4), 2014.
Sam Lindley and J. Garrett Morris. A semantics for propositions as sessions. In European Symposium On Programming (ESOP), pages 560-584, 2015.
Sam Lindley and J. Garrett Morris. Talking bananas: structural recursion for session types. In International Colloquium on Functional Progrmaming (ICFP), pages 434-447, 2016.
Robin Milner. Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, 1999.
Uwe Nestmann. What is a "good" encoding of guarded choice? Inf. Comput., 156(1-2):287-319, 2000.
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.
Catuscia Palamidessi. Comparing the expressive power of the synchronous and asynchronous pi-calculi. Mathematical Structures in Computer Science, 13(5):685-719, 2003.
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.
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.
Jason Reed. A judgmental deconstruction of modal logic. Unpublished manuscript, January 2009. URL: http://www.cs.cmu.edu/~jcreed/papers/jdml.pdf.
http://www.cs.cmu.edu/~jcreed/papers/jdml.pdf
Davide Sangiorgi and David Walker. The π-Calculus - A Theory of Mobile Processes. Cambridge University Press, 2001.
Bernardo Toninho. A Logical Foundation for Session-based Concurrent Computation. PhD thesis, Carnegie Mellon University and New University of Lisbon, 2015.
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.
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.
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.
Philip Wadler. Propositions as sessions. In 17th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 273-286. ACM, 2012.
Stephanie Balzer, Frank Pfenning, and Bernardo Toninho
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode