research-article

Open access

Termination in Concurrency, Revisited

Authors:

Joseph W. N. Paulus,

Jorge A. Pérez,

Daniele Nantes-SobrinhoAuthors Info & Claims

PPDP '23: Proceedings of the 25th International Symposium on Principles and Practice of Declarative Programming

Article No.: 3, Pages 1 - 14

https://doi.org/10.1145/3610612.3610615

Published: 22 October 2023 Publication History

All formats PDF

Abstract

Termination is a central property in sequential programming models: a term is terminating if all its reduction sequences are finite. Termination is also important in concurrency in general, and for message-passing programs in particular. A variety of type systems that enforce termination by typing have been developed. In this paper, we rigorously compare several type systems for π -calculus processes from the unifying perspective of termination. Adopting session types as reference framework, we consider two different type systems: one follows Deng and Sangiorgi’s weight-based approach; the other is Caires and Pfenning’s Curry-Howard correspondence between linear logic and session types. Our technical results precisely connect these very different type systems, and shed light on the classes of client/server interactions they admit as correct.

References

[1]

Luís Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In CONCUR 2010(LNCS, Vol. 6269). Springer, 222–236. https://doi.org/10.1007/978-3-642-15375-4_16

[2]

Ornela Dardha, Elena Giachino, and Davide Sangiorgi. 2012. Session types revisited. In PPDP’12. ACM, 139–150. https://doi.org/10.1145/2370776.2370794

Digital Library

[3]

Ornela Dardha and Jorge A. Pérez. 2015. Comparing Deadlock-Free Session Typed Processes. In Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics, and 12th Workshop on Structural Operational Semantics, EXPRESS/SOS(EPTCS, Vol. 190). 1–15. https://doi.org/10.4204/EPTCS.190.1

[4]

Ornela Dardha and Jorge A. Pérez. 2022. Comparing type systems for deadlock freedom. J. Log. Algebraic Methods Program. 124 (2022), 100717. https://doi.org/10.1016/j.jlamp.2021.100717

[5]

Romain Demangeon, Daniel Hirschkoff, and Davide Sangiorgi. 2010. Termination in Impure Concurrent Languages. In CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings(Lecture Notes in Computer Science, Vol. 6269), Paul Gastin and François Laroussinie (Eds.). Springer, 328–342. https://doi.org/10.1007/978-3-642-15375-4_23

[6]

Yuxin Deng and Davide Sangiorgi. 2004. Ensuring Termination by Typability. In Exploring New Frontiers of Theoretical Informatics, IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004), 22-27 August 2004, Toulouse, France(IFIP, Vol. 155), Jean-Jacques Lévy, Ernst W. Mayr, and John C. Mitchell (Eds.). Kluwer/Springer, 619–632. https://doi.org/10.1007/1-4020-8141-3_47

[7]

Yuxin Deng and Davide Sangiorgi. 2006. Ensuring termination by typability. Information and Computation 204, 7 (2006), 1045–1082.

Digital Library

[8]

Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. In ESOP’98(LNCS, Vol. 1381). Springer, 122–138. https://doi.org/10.1007/BFb0053567

[9]

Naoki Kobayashi and Davide Sangiorgi. 2010. A hybrid type system for lock-freedom of mobile processes. ACM Trans. Program. Lang. Syst. 32, 5 (2010), 16:1–16:49. https://doi.org/10.1145/1745312.1745313

Digital Library

[10]

Ugo Dal Lago, Marc de Visme, Damiano Mazza, and Akira Yoshimizu. 2019. Intersection types and runtime errors in the pi-calculus. Proc. ACM Program. Lang. 3, POPL (2019), 7:1–7:29. https://doi.org/10.1145/3290320

Digital Library

[11]

Joseph W. N. Paulus, Jorge A. Pérez, and Daniele Nantes-Sobrinho. 2023. Termination in Concurrency, Revisited. (2023). arxiv:2308.01165https://doi.org/10.48550/arXiv.2308.01165

[12]

Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. 2014. Linear logical relations and observational equivalences for session-based concurrency. Inf. Comput. 239 (2014), 254–302. https://doi.org/10.1016/j.ic.2014.08.001

Digital Library

[13]

Mauro Piccolo. 2012. Strong Normalization in the π -calculus with Intersection and Union Types. Fundam. Informaticae 121, 1-4 (2012), 227–252. https://doi.org/10.3233/FI-2012-777

[14]

Davide Sangiorgi. 2006. Termination of processes. Math. Struct. Comput. Sci. 16, 1 (2006), 1–39. https://doi.org/10.1017/S0960129505004810

Digital Library

[15]

Bernardo Toninho, Luís Caires, and Frank Pfenning. 2014. 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(Lecture Notes in Computer Science, Vol. 8902), Matteo Maffei and Emilio Tuosto (Eds.). Springer, 159–175. https://doi.org/10.1007/978-3-662-45917-1_11

[16]

Vasco T. Vasconcelos. 2012. Fundamentals of session types. Inf. Comput. 217 (2012), 52–70. https://doi.org/10.1016/j.ic.2012.05.002

Digital Library

[17]

Nobuko Yoshida, Martin Berger, and Kohei Honda. 2001. Strong Normalisation in the pi-Calculus. In 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings. IEEE Computer Society, 311–322. https://doi.org/10.1109/LICS.2001.932507

Cited By

Dagnino FPadovani L(2024)sMALL CaPS: An Infinitary Linear Logic for a Calculus of Pure SessionsProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678234(1-13)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678234

Index Terms

Termination in Concurrency, Revisited
1. Theory of computation
  1. Models of computation
    1. Concurrency
      1. Process calculi
  2. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

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 ...
Minimal Session Types for the π-calculus
PPDP '21: Proceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming

Session types enable the static verification of message-passing programs. A session type specifies a channel’s protocol as sequences of messages. Prior work established a minimality result: every process typable with standard session types can be ...
Session types revisited
PPDP '12: Proceedings of the 14th symposium on Principles and practice of declarative programming

Session types are a formalism to model structured communication-based programming. A session type describes communication by specifying the type and direction of data exchanged between two parties. When session types and session primitives are added to ...

Comments

Information & Contributors

Information

Published In

cover image ACM Other conferences

PPDP '23: Proceedings of the 25th International Symposium on Principles and Practice of Declarative Programming

October 2023

173 pages

ISBN:9798400708121

DOI:10.1145/3610612

Editors:
Santiago Escobar
Universitat Politècnica de València, Valencia, Spain
,
Vasco T. Vasconcelos
LASIGE, University of Lisbon

Copyright © 2023 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 the author(s) 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].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 October 2023

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Funding Sources

Conference

PPDP 2023

PPDP 2023: International Symposium on Principles and Practice of Declarative Programming

October 22 - 23, 2023

Lisboa, Portugal

Acceptance Rates

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
193
Total Downloads

Downloads (Last 12 months)173
Downloads (Last 6 weeks)13

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Dagnino FPadovani L(2024)sMALL CaPS: An Infinitary Linear Logic for a Calculus of Pure SessionsProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678234(1-13)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678234

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents