Interleaving sessions with predicates
Pages 1312 - 1318
Abstract
We propose an extension of binary session types with interleaved sessions that work similar to interrupts. The participants in a session register a set of trigger predicates that are associated with local protocols. When a trigger fires, all participants switch simultaneously to the interleaved protocol and return to the original protocol afterwards. The use of interleaved sessions enables the elegant specification of protocols that are otherwise cumbersome to specify.
References
[1]
L. Caires and F. Pfenning. Session types as intuitionistic linear propositions. In CONCUR, volume 6269 of LNCS, pages 222--236, Paris, France, Aug. 2010. Springer.
[2]
S. Capecchi, E. Giachino, and N. Yoshida. Global escape in multiparty sessions. Mathematical Structures in Computer Science, 26(2):156--205, 2016.
[3]
M. Carbone, K. Honda, and N. Yoshida. Structured interactional exceptions in session types. In F. van Breugel and M. Chechik, editors, CONCUR, volume 5201 of LNCS, pages 402--417. Springer, 2008.
[4]
M. Carbone, N. Yoshida, and K. Honda. Asynchronous session types: Exceptions and multiparty interactions. In M. Bernardo, L. Padovani, and G. Zavattaro, editors, SFM, volume 5569 of LNCS, pages 187--212. Springer, 2009.
[5]
I. Castellani, M. Dezani-Ciancaglini, and J. A. Pérez. Self-adaptation and secure information flow in multiparty communications. Formal Asp. Comput., 28(4):669--696, 2016.
[6]
T. Chen, M. Viering, A. Bejleri, L. Ziarek, and P. Eugster. A type theory for robust failure handling in distributed systems. In FORTE, volume 9688 of LNCS, pages 96--113. Springer, 2016.
[7]
R. Demangeon, K. Honda, R. Hu, R. Neykova, and N. Yoshida. Practical interruptible conversations: Distributed dynamic verification with multiparty session types and Python. Formal Methods in System Design, 46(3):197--225, 2015.
[8]
M. Dezani-Ciancaglini, S. Drossopoulou, D. Mostrous, and N. Yoshida. Objects and session types. Information and Computation, 207(5):595--641, 2009.
[9]
S. J. Gay and M. J. Hole. Types and subtypes for client-server interactions. In Proc. 1999 ESOP, volume 1576 of LNCS, pages 74--90, Amsterdam, The Netherlands, Apr. 1999. Springer.
[10]
S. J. Gay and V. T. Vasconcelos. Linear type theory for asynchronous session types. J. Fund. Program., 20(1):19--50, 2010.
[11]
S. J. Gay, V. T. Vasconcelos, A. Ravara, N. Gesbert, and A. Z. Caldeira. Modular session types for distributed object-oriented programming. In Proc. 37th ACM Symp. POPL, pages 299--312, Madrid, Spain, Jan. 2010. ACM Press.
[12]
K. Honda. Types for dyadic interaction. In E. Best, editor, Proceedings of 4th International Conference on Concurrency Theory, number 715 in LNCS, pages 509--523, Aug. 1993.
[13]
K. Honda, A. Mukhamedov, G. Brown, T.-C. Chen, and N. Yoshida. Scribbling interactions with a formal foundation. In ICDCIT 2011, volume 6536 of LNCS, pages 55--75, Bhubaneshwar, India, 2011. Springer.
[14]
K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. In P. Wadler, editor, Proc. 35th ACM Symp. POPL, pages 273--284, San Francisco, CA, USA, Jan. 2008. ACM Press.
[15]
L. Padovani. Context-Free Session Type Inference, working paper or preprint, Oct. 2016.
[16]
V. T. Vasconcelos, A. Ravara, and S. J. Gay. Type checking a multithreaded functional language with session types. Theoretical Computer Science, 368(1--2):64--87, 2006.
[17]
P. Wadler. Propositions as sessions. In R. B. Findler, editor, ICFP'12, pages 273--286, Copenhagen, Denmark, Sept. 2012. ACM.
Index Terms
- Interleaving sessions with predicates
Recommendations
Multiparty GV: functional multiparty session types with certified deadlock freedom
Session types have recently been integrated with functional languages, bringing message-passing concurrency to functional programming. Channel endpoints then become first-class and can be stored in data structures, captured in closures, and sent along ...
Effects as sessions, sessions as effects
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesEffect and session type systems are two expressive behavioural type systems. The former is usually developed in the context of the lambda-calculus and its variants, the latter for the pi-calculus. In this paper we explore their relative expressive ...
A bunch of sessions: a propositions-as-sessions interpretation of bunched implications in channel-based concurrency
The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical foundations of message-passing concurrency. Central to this approach is the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
April 2017
2004 pages
ISBN:9781450344869
DOI:10.1145/3019612
- Conference Chair:
- Sung Y. Shin,
- Program Chairs:
- Dongwan Shin,
- Maria Lencastre
Copyright © 2017 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 03 April 2017
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
SAC 2017
Sponsor:
Acceptance Rates
Overall Acceptance Rate 1,650 of 6,669 submissions, 25%
Upcoming Conference
SAC '25
- Sponsor:
- sigapp
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 49Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 19 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in