Message-Observing Sessions
Article No.: 142, Pages 1351 - 1379
Abstract
We present Most, a process language with message-observing session types. Message-observing session types extend binary session types with type-level computation to specify communication protocols that vary based on messages observed on other channels. Hence, Most allows us to express global invariants about processes, rather than just local invariants, in a bottom-up, compositional way. We give Most a semantic foundation using traces with binding, a semantic approach for compositionally reasoning about traces in the presence of name generation. We use this semantics to prove type soundness and compositionality for Most processes. We see this as a significant step towards capturing message-dependencies and providing more precise guarantees about processes.
References
[1]
Robert Atkey. 2017. “ Observed Communication Semantics for Classical Processes”. In: Programming Languages and Systems (Lecture Notes in Computer Science) 10201. 26th European Symposium on Programming. ESOP 2017 ( Uppsala, Sweden, Apr. 22-29, 2017 ). Ed. by Hongseok Yang. Springer-Verlag GmbH Germany, Berlin, Germany, 56-82. isbn: 978-3-662-54434-1. https://doi.org/10.1007/978-3-662-54434-1_3.
[2]
Stephanie Balzer and Frank Pfenning. Sept. 2017. “ Manifest Sharing With Session Types”. Proceedings of the ACM on Programming Languages, 1, ICFP, ( Sept. 2017 ), 37. https://doi.org/10.1145/3110281.
[3]
Luís Caires and Frank Pfenning. 2010. “ Session Types as Intuitionistic Linear Propositions”. In: CONCUR 2010-Concurrency Theory (Lecture Notes in Computer Science ) 6269. 21st International Conference, CONCUR 2010 (Paris, France, Aug. 31-Sept. 3, 2010 ). Ed. by Paul Gastin and François Laroussinie. Springer-Verlag Berlin Heidelberg, 222-236. isbn: 978-3-642-15374-7. https://doi.org/10.1007/978-3-642-15375-4_16.
[4]
Luís Caires, Frank Pfenning, and Bernardo Toninho. Mar. 2016. “ Linear Logic Propositions As Session Types”. Mathematical Structures in Computer Science, 26, 3, ( Mar. 2016 ), 367-423. Behavioural Types Part 2. https://doi.org/10.1017/s09601295140 00218.
[5]
Iliano Cervesato and Andre Scedrov. Oct. 2009. “ Relating State-Based and Process-Based Concurrency Through Linear Logic (Full-Version)”. Information and Computation, 207, 10, (Oct. 2009 ), 1044-1077. Special Issue: 13th Workshop on Logic, Language, Information and Computation (WoLLIC 2006 ). https://doi.org/10.1016/j.ic. 2008. 11.006.
[6]
Silvia Crafa, Daniele Varacca, and Nobuko Yoshida. 2007. “ Compositional Event Structure Semantics for the Internal-Calculus”. In: CONCUR 2007-Concurrency Theory (Lecture Notes in Computer Science) 4703. 18th International Conference on Concurrency Theory. CONCUR 2007 (Lisbon, Portugal, Sept. 3-8, 2007 ). Ed. by Luís Caires and Vasco T. Vasconcelos. Springer-Verlag Berlin Heidelberg, 317-332. isbn: 978-3-540-74407-8. https://doi.org/10.1007/978-3-540-744 07-8_22.
[7]
Pierre-Malo Deniélou and Nobuko Yoshida. 2011. “ Dynamic Multirole Session Types”. In: POPL'11. 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL'11 (Austin, Texas, Jan. 26-28, 2011 ). Association for Computing Machinery, Inc., New York, New York, 435-446. isbn: 978-1-4503-0490-0. https://doi.org/10.11 45/1926385.1926435.
[8]
Farzaneh Derakhshan and Frank Pfenning. May 10, 2022. “ Circular Proofs As Session-Typed Processes: A Local Validity Condition”. Logical Methods in Computer Science, 18, 2, (May 10, 2022 ), 8. https://doi.org/10.46298/lmcs-18 ( 2 :8) 2022.
[9]
Thomas Ehrhard. Aug. 2018. “An Introduction To Diferential Linear Logic: Proof-Nets, Models and Antiderivatives”. Mathematical Structures in Computer Science, 28, 7, ( Aug. 2018 ), 995-1060. Diferential Linear Logic, Nets and Other Quantitative and Parallel Approaches to Proof-Theory. https://doi.org/10.1017/s0960129516000372.
[10]
Murdoch Gabbay and Dan Ghica. Sept. 24, 2012. “ Game Semantics in the Nominal Model”. Electronic Notes in Theoretical Computer Science, 286, (Sept. 24, 2012 ), 173-189. Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII). https://doi.org/10.1016/j.entcs. 2012. 08.012.
[11]
Kohei Honda. 1993. “ Types for Dyadic Interaction”. In: CONCUR'93 (Lecture Notes in Computer Science) 715. 4th International Conference on Concurrency Theory (Hildesheim, Germany, Aug. 23-26, 1993 ). Ed. by Eike Best. Springer-Verlag Berlin Heidelberg, Berlin, 509-523. isbn: 978-3-540-47968-0. https://doi.org/10.1007/3-540-57208-2_35.
[12]
Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. 1998. “Language Primitives and Type Discipline for Structured Communication-Based Programming”. In: Programming Languages and Systems (Lecture Notes in Computer Science) 1381. 7th European Symposium on Programming. ESOP'98 (Lisbon, Portugal, Mar. 28-Apr. 4, 1998 ). Ed. by Chris Hankin. Joint European Conferences on Theory and Practice of Software, ETAPS'98. Springer-Verlag Berlin Heidelberg, 122-138. isbn: 978-3-540-69722-0. https://doi.org/10.1007/BFb0053567.
[13]
Kohei Honda, Nobuko Yoshida, and Marco Carbone. Mar. 3, 2016. “ Multiparty Asynchronous Session Types”. Journal of the ACM, 63, 1, ( Mar. 3, 2016 ), 9. https://doi.org/10.1145/2827695.
[14]
Ryan Kavanagh. May 2022. “ Fairness and Communication-Based Semantics for Session-Typed Languages”. Information and Computation, 285, B, (May 2022 ), 104892. https://doi.org/10.1016/j.ic. 2022. 104892.
[15]
Ryan Kavanagh and Brigitte Pientka. Mar. 8, 2024. Message-Observing Sessions. (Mar. 8, 2024 ). arXiv: 2403.04633 [cs.PL].
[16]
Benjamin Pierce. 2002. Types and Programming Languages. The MIT Press, Cambridge, Massachusetts. xxi+623 pp. isbn: 0-262-16209-1.
[17]
Pedro Rocha and Luís Caires. Aug. 2021. “ Propositions-As-Types and Shared State”. Proceedings of the ACM on Programming Languages, 5, ICFP, ( Aug. 2021 ), 79. https://doi.org/10.1145/3473584.
[18]
Pedro Rocha and Luís Caires. 2023. “ Safe Session-Based Concurrency With Shared Linear State”. In: Programming Languages and Systems (Lecture Notes in Computer Science) 13990. 32nd European Symposium on Programming. ESOP 2023 (Paris, France, Apr. 22-27, 2023 ). Ed. by Thomas Wies. Springer, Cham, Switzerland, 421-450. isbn: 978-3-031-30044-8. https://doi.org/10.1007/978-3-031-30044-8_16.
[19]
Siva Somayyajula and Frank Pfenning. 2022. “ Type-Based Termination for Futures”. In: 7th International Conference on Formal Structures for Computation and Deduction (Leibniz International Proceedings in Informatics (LIPIcs)). 7th International Conference on Formal Structures for Computation and Deduction. FSCD 2022 ( Haifa, Israel, Aug. 2-5, 2022 ). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Saarbrücken/Wadern, Germany. isbn: 978-3-95977-233-4. https://doi.org/10.4230/LIPIcs.FSCD. 2022. 12.
[20]
Claude Stolze, Marino Miculan, and Pietro Di Gianantonio. Apr. 2023. “ Composable Partial Multiparty Session Types for Open Systems”. Software and Systems Modeling, 22, 2, ( Apr. 2023 ), 473-494. https://doi.org/10.1007/s10270-022-01040-x.
[21]
Kaku Takeuchi, Kohei Honda, and Makoto Kubo. 1994. “An Interaction-Based Language and Its Typing System”. In: PARLE'94. Parallel Architectures and Languages Europe (Lecture Notes in Computer Science) 10201. 6th International PARLE Conference (Athens, Greece, July 4-8, 1994 ). Ed. by Costas Halatsis, Dimitrios Maritsas, George Philokyprou, and Sergios Theodoridis. Springer-Verlag Berlin Heidelberg, Berlin, 398-413. isbn: 978-3-540-48477-6. https://doi.org/10.1007 /3-540-58184-7_118.
[22]
The Go Project. Feb. 6, 2024. The Go Programming Language Specification. Language version go1.22. (Feb. 6, 2024 ). Retrieved Mar. 5, 2024 from https://perma.cc/436Q-ZL6J.
[23]
Peter Thiemann and Vasco T. Vasconcelos. Dec. 2019. “ Label-Dependent Session Types”. Proceedings of the ACM on Programming Languages, 4, POPL, ( Dec. 2019 ), 67. https://doi.org/10.1145/3371135.
[24]
Bernardo Toninho, Luís Caires, and Frank Pfenning. 2011. “ Dependent Session Types Via Intuitionistic Linear Type Theory”. In: PPDP'11. 13th International ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming. PPDP'11 (Odense, Denmark, July 20-22, 2011 ). Association for Computing Machinery, Inc., New York, New York, 161-172. isbn: 978-1-4503-0776-5. https://doi.org/10.1145/2003476.2003499.
[25]
Bernardo Toninho and Nobuko Yoshida. 2018. “Depending on Session-Typed Processes”. In: Foundations of Software Science and Computation Structures (Lecture Notes in Computer Science ) 10803. 21st International Conference, FOSSACS 2018 (Thessaloniki, Greece, Apr. 14-20, 2018 ). Ed. by Christel Baier and Ugo Dal Lago. European Joint Conferences on Theory and Practice of Software. SpringerOpen, Cham, Switzerland, 128-145. isbn: 978-3-319-89 3-319-89366-2_7.
[26]
Daniele Varacca and Nobuko Yoshida. Apr. 6, 2010. “ Typed Event Structures and the Linear-calculus”. Theoretical Computer Science, 411, 19, ( Apr. 6, 2010 ), 1949-1973. Mathematical Foundations of Programming Semantics (MFPS 2006 ). https://doi.org/10.1016/j.tcs. 2010. 01.024.
[27]
Philip Wadler. Jan. 31, 2014. “ Propositions As Sessions”. Journal of Functional Programming, 24, 2-3, (Jan. 31, 2014 ), 384-418. https://doi.org/10.1017/s095679681400001x.
Recommendations
Intrinsically-Typed Mechanized Semantics for Session Types
PPDP '19: Proceedings of the 21st International Symposium on Principles and Practice of Declarative ProgrammingSession types have emerged as a powerful paradigm for structuring communication-based programs. They guarantee type soundness and session fidelity for concurrent programs with sophisticated communication protocols. As type soundness proofs for languages ...
Intrinsically Typed Sessions with Callbacks (Functional Pearl)
All formalizations of session types rely on linear types for soundness as session-typed communication channels must change their type at every operation. Embedded language implementations of session types follow suit. They either rely on clever typing ...
Label-dependent session types
Session types have emerged as a typing discipline for communication protocols. Existing calculi with session types come equipped with many different primitives that combine communication with the introduction or elimination of the transmitted value.
We ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
April 2024
1492 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 29 April 2024
Published in PACMPL Volume 8, Issue OOPSLA1
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- Natural Sciences and Engineering Research Council of Canada
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 156Total Downloads
- Downloads (Last 12 months)156
- Downloads (Last 6 weeks)56
Reflects downloads up to 10 Nov 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in