More Web Proxy on the site http://driver.im/

research-article

Open access

Parameterized Algebraic Protocols

Authors:

Andreia Mordido,

Janek Spaderna,

Peter Thiemann,

Vasco T. VasconcelosAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 7, Issue PLDI

Article No.: 163, Pages 1389 - 1413

https://doi.org/10.1145/3591277

Published: 06 June 2023 Publication History

Abstract

We propose algebraic protocols that enable the definition of protocol templates and session types analogous to the definition of domain-specific types with algebraic datatypes. Parameterized algebraic protocols subsume all regular as well as most context-free and nested session types and, at the same time, replace the expensive superlinear algorithms for type checking by a nominal check that runs in linear time. Algebraic protocols in combination with polymorphism increase expressiveness and modularity by facilitating new ways of parameterizing and composing session types.

References

[1]

Martín Abadi and Marcelo P. Fiore. 1996. Syntactic Considerations on Recursive Types. In 11th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, New Brunswick, New Jersey, USA. 242–252. https://doi.org/10.1109/LICS.1996.561324

[2]

Bernardo Almeida, Andreia Mordido, Peter Thiemann, and Vasco T. Vasconcelos. 2022. Polymorphic Lambda Calculus with Context-Free Session Types. Information and Computation, https://doi.org/10.1016/j.ic.2022.104948

Digital Library

[3]

Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconcelos. 2019. FreeST: Context-free Session Types in a Functional Language. In PLACES@ETAPS 2019, Francisco Martins and Dominic Orchard (Eds.) (EPTCS, Vol. 291). Prague, Czech Republic. 12–23. https://doi.org/10.4204/EPTCS.291.2

[4]

Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconcelos. 2020. Deciding the Bisimilarity of Context-Free Session Types. In TACAS 2020, Armin Biere and David Parker (Eds.) (Lecture Notes in Computer Science, Vol. 12079). Springer, Dublin, Ireland. 39–56. https://doi.org/10.1007/978-3-030-45237-7_3

Digital Library

[5]

Sandra Alves, Maribel Fernández, Mário Florido, and Ian Mackie. 2010. Linearity and iterator types for Gödel’s System. High. Order Symb. Comput., 23, 1 (2010), 1–27. https://doi.org/10.1007/s10990-010-9060-x

Digital Library

[6]

Robert Atkey. 2018. Syntax and Semantics of Quantitative Type Theory. In LICS 2018, Anuj Dawar and Erich Grädel (Eds.). ACM, Oxford, UK. 56–65. https://doi.org/10.1145/3209108.3209189

Digital Library

[7]

Massimo Bartoletti, Alceste Scalas, and Roberto Zunino. 2014. A Semantic Deconstruction of Session Types. In CONCUR 2014, Paolo Baldan and Daniele Gorla (Eds.) (Lecture Notes in Computer Science, Vol. 8704). Springer, Rome, Italy. 402–418. https://doi.org/10.1007/978-3-662-44584-6_28

[8]

Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. 2018. Linear Haskell: practical linearity in a higher-order polymorphic language. Proc. ACM Program. Lang., 2, POPL (2018), 5:1–5:29. https://doi.org/10.1145/3158093

Digital Library

[9]

Rod M. Burstall. 1977. Design Considerations for a Functional Programming Language. In Infotech State of the Art Conference: The Software Revolution. Copenhagen.

[10]

Rod M. Burstall, David B. MacQueen, and Donald Sannella. 1980. HOPE: An Experimental Applicative Language. In Proceedings of the 1980 LISP Conference. ACM, Stanford, California, USA. 136–143. https://doi.org/10.1145/800087.802799

Digital Library

[11]

Luís Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In CONCUR 2010, Paul Gastin and François Laroussinie (Eds.) (Lecture Notes in Computer Science, Vol. 6269). Springer, Paris, France. 222–236. https://doi.org/10.1007/978-3-642-15375-4_16

[12]

Luís Caires, Frank Pfenning, and Bernardo Toninho. 2016. Linear Logic Propositions as Session Types. Math. Struct. Comput. Sci., 26, 3 (2016), 367–423. https://doi.org/10.1017/S0960129514000218

[13]

Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Elena Giachino, and Luca Padovani. 2009. Foundations of Session Types. In PPDP 2009, António Porto and Francisco Javier López-Fraguas (Eds.). ACM, Coimbra, Portugal. 219–230. https://doi.org/10.1145/1599410.1599437

Digital Library

[14]

Diana Costa, Andreia Mordido e Diogo Poças, and Vasco T. Vasconcelos. 2023. System F^μ _ω with Context-free Session Types. In Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Proceedings (Lecture Notes in Computer Science). Springer. To appear

[15]

Diana Costa, Andreia Mordido, Diogo Poças, and Vasco T. Vasconcelos. 2022. Higher-order Context-free Session Types in System F. In Proceedings of the 13th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES@ETAPS 2022, Munich, Germany, 3rd April 2022, Marco Carbone and Rumyana Neykova (Eds.) (EPTCS, Vol. 356). 24–35. https://doi.org/10.4204/EPTCS.356.3

[16]

Olivier Danvy and Andrzej Filinski. 1992. Representing Control: A Study of the CPS Transformation. Math. Struct. Comput. Sci., 2, 4 (1992), 361–391. https://doi.org/10.1017/S0960129500001535

[17]

Ankush Das, Henry DeYoung, Andreia Mordido, and Frank Pfenning. 2021. Nested Session Types. In Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Nobuko Yoshida (Ed.) (Lecture Notes in Computer Science, Vol. 12648). Springer, Luxembourg City, Luxembourg. 178–206. https://doi.org/10.1007/978-3-030-72019-3_7

Digital Library

[18]

Jana Dunfield and Neel Krishnaswami. 2021. Bidirectional Typing. ACM Comput. Surv., 54, 5 (2021), 98:1–98:38. https://doi.org/10.1145/3450952

Digital Library

[19]

Matthias Felleisen. 1988. The Theory and Practice of First-Class Prompts. In POPL, Jeanne Ferrante and Peter Mager (Eds.). ACM Press, San Diego, California, USA. 180–190. https://doi.org/10.1145/73560.73576

Digital Library

[20]

Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. 2021. Separating Sessions Smoothly. In 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Serge Haddad and Daniele Varacca (Eds.) (LIPIcs, Vol. 203). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Virtual Conference. 36:1–36:18. https://doi.org/10.4230/LIPIcs.CONCUR.2021.36

[21]

Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. 2021. Separating Sessions Smoothly. CoRR, abs/2105.08996 (2021), arXiv:2105.08996. https://doi.org/10.48550/arXiv.2105.08996

[22]

(last accessed March 2023). The FreeST Programming Language. https://freest-lang.github.io/

[23]

Simon J. Gay and Malcolm Hole. 1999. Types and Subtypes for Client-Server Interactions. In Programming Languages and Systems, 8th European Symposium on Programming, ESOP’99, S. Doaitse Swierstra (Ed.) (Lecture Notes in Computer Science, Vol. 1576). Springer, Amsterdam, The Netherlands. 74–90. https://doi.org/10.1007/3-540-49099-X_6

[24]

Simon J. Gay and Malcolm Hole. 2005. Subtyping for Session Types in the Pi Calculus. Acta Informatica, 42, 2-3 (2005), 191–225. https://doi.org/10.1007/s00236-005-0177-z

[25]

Simon J. Gay, Diogo Poças, and Vasco T. Vasconcelos. 2022. The Different Shades of Infinite Session Types. In FOSSACS 2022, Patricia Bouyer and Lutz Schröder (Eds.) (Lecture Notes in Computer Science, Vol. 13242). Springer, Munich, Germany. 347–367. https://doi.org/10.1007/978-3-030-99253-8_18

Digital Library

[26]

Simon J. Gay and Vasco Thudichum Vasconcelos. 2010. Linear Type Theory for Asynchronous Session Types. J. Funct. Program., 20, 1 (2010), 19–50. https://doi.org/10.1017/S0956796809990268

Digital Library

[27]

Kohei Honda. 1993. Types for Dyadic Interaction. In CONCUR ’93, Eike Best (Ed.) (Lecture Notes in Computer Science, Vol. 715). Springer, Hildesheim, Germany. 509–523. https://doi.org/10.1007/3-540-57208-2_35

[28]

Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. In Programming Languages and Systems - ESOP’98, 7th European Symposium on Programming, Chris Hankin (Ed.) (Lecture Notes in Computer Science, Vol. 1381). Springer, Lisbon, Portugal. 122–138. https://doi.org/10.1007/BFb0053567

[29]

Simon L. Peyton Jones, Andrew D. Gordon, and Sigbjørn Finne. 1996. Concurrent Haskell. In POPL’96, Hans-Juergen Boehm and Guy L. Steele Jr. (Eds.). ACM Press, St. Petersburg Beach, Florida, USA. 295–308. https://doi.org/10.1145/237721.237794

Digital Library

[30]

Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. 2015. Integrating Linear and Dependent Types. In POPL 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, Mumbai, India. 17–30. https://doi.org/10.1145/2676726.2676969

Digital Library

[31]

Sam Lindley and J. Garrett Morris. 2016. Talking bananas: structural recursion for session types. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, Nara, Japan. 434–447. https://doi.org/10.1145/2951913.2951921

Digital Library

[32]

Sam Lindley and J. Garrett Morris. 2017. Lightweight Functional Session Types. In Behavioural Types: from Theory to Tools, Simon Gay and António Ravara (Eds.). River Publishers, Gistrup, Denmark. Extended version at https://homepages.inf.ed.ac.uk/slindley/papers/fst-extended.pdf

[33]

Karl Mazurak, Jianzhou Zhao, and Steve Zdancewic. 2010. Lightweight linear types in system fdegree. In TLDI 2010, Andrew Kennedy and Nick Benton (Eds.). ACM, Madrid, Spain. 77–88. https://doi.org/10.1145/1708016.1708027

Digital Library

[34]

Conor McBride. 2016. I Got Plenty o’ Nuttin’. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella (Eds.) (Lecture Notes in Computer Science, Vol. 9600). Springer, Edinburgh, Scotland. 207–233. https://doi.org/10.1007/978-3-319-30936-1_12

[35]

Robin Milner, Joachim Parrow, and David Walker. 1992. A Calculus of Mobile Processes, II. Inf. Comput., 100, 1 (1992), 41–77. https://doi.org/10.1016/0890-5401(92)90009-5

Digital Library

[36]

Fabrizio Montesi and Marco Peressotti. 2021. Linear Logic, the π -calculus, and their Metatheory: A Recipe for Proofs as Processes. CoRR, abs/2106.11818 (2021), arXiv:2106.11818. arxiv:2106.11818

[37]

Andreia Mordido, Janek Spaderna, Peter Thiemann, and Vasco T. Vasconcelos. 2023. Parameterized Algebraic Protocols. arxiv:2304.03764. https://doi.org/10.48550/arXiv.2304.03764

[38]

Bryan O’Sullivan. (last accessed March 2023). gauge: small framework for performance measurement and analysis. https://hackage.haskell.org/package/gauge-0.2.5/

[39]

Luca Padovani. 2017. Context-Free Session Type Inference. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Hongseok Yang (Ed.) (Lecture Notes in Computer Science, Vol. 10201). Springer, Uppsala, Sweden. 804–830. https://doi.org/10.1007/978-3-662-54434-1_30

Digital Library

[40]

Luca Padovani. 2019. Context-Free Session Type Inference. ACM Trans. Program. Lang. Syst., 41, 2 (2019), 9:1–9:37. https://doi.org/10.1145/3229062

Digital Library

[41]

Marco Patrignani, Eric Mark Martin, and Dominique Devriese. 2021. On the Semantic Expressiveness of Recursive Types. Proc. ACM Program. Lang., 5, POPL (2021), 1–29. https://doi.org/10.1145/3434302

Digital Library

[42]

Frank Pfenning, Luís Caires, and Bernardo Toninho. 2011. Proof-Carrying Code in a Session-Typed Process Calculus. In CPP 2011, Jean-Pierre Jouannaud and Zhong Shao (Eds.) (Lecture Notes in Computer Science, Vol. 7086). Springer, Kenting, Taiwan. 21–36. https://doi.org/10.1007/978-3-642-25379-9_4

Digital Library

[43]

Frank Pfenning and Dennis Griffith. 2015. Polarized Substructural Session Types. In FoSSaCS 2015, Andrew M. Pitts (Ed.) (Lecture Notes in Computer Science, Vol. 9034). Springer, London, UK. 3–22. https://doi.org/10.1007/978-3-662-46678-0_1

[44]

Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press. isbn:978-0-262-16209-8

Digital Library

[45]

Janek Spaderna, Peter Thiemann, Andreia Mordido, and Vasco T. Vasconcelos. 2023. Parametrized Algebraic Protocols: Artifact. https://doi.org/10.5281/zenodo.7804667

Digital Library

[46]

Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, and Richard A. Eisenberg. 2022. Linearly qualified types: generic inference for capabilities and uniqueness. Proc. ACM Program. Lang., 6, ICFP (2022), 137–164. https://doi.org/10.1145/3547626

Digital Library

[47]

Kaku Takeuchi, Kohei Honda, and Makoto Kubo. 1994. An Interaction-based Language and its Typing System. In PARLE ’94, Constantine Halatsis, Dimitris G. Maritsas, George Philokyprou, and Sergios Theodoridis (Eds.) (Lecture Notes in Computer Science, Vol. 817). Springer, Athens, Greece. 398–413. https://doi.org/10.1007/3-540-58184-7_118

[48]

Peter Thiemann and Vasco T. Vasconcelos. 2016. Context-free Session Types. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, Nara, Japan. 462–475. https://doi.org/10.1145/2951913.2951926

Digital Library

[49]

Peter Thiemann and Vasco T. Vasconcelos. 2020. Label-dependent session types. Proc. ACM Program. Lang., 4, POPL (2020), 67:1–67:29. https://doi.org/10.1145/3371135

Digital Library

[50]

Bernardo Toninho, Luís Caires, and Frank Pfenning. 2013. Higher-Order Processes, Functions, and Sessions: A Monadic Integration. In Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Matthias Felleisen and Philippa Gardner (Eds.) (Lecture Notes in Computer Science, Vol. 7792). Springer, Rome, Italy. 350–369. https://doi.org/10.1007/978-3-642-37036-6_20

Digital Library

[51]

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, Matteo Maffei and Emilio Tuosto (Eds.) (Lecture Notes in Computer Science, Vol. 8902). Springer, Rome, Italy. 159–175. https://doi.org/10.1007/978-3-662-45917-1_11

[52]

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

[53]

David Walker. 2005. Advanced Topics in Types and Programming Languages. The MIT Press, 3–44.

Cited By

Ângelo PIgarashi AT. Vasconcelos V(2024)Linear Contextual Metaprogramming and Session TypesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.401.1401(1-10)Online publication date: 6-Apr-2024
https://doi.org/10.4204/EPTCS.401.1
Pham LWang DSaad FHoffmann J(2024)Programmable MCMC with Soundly Composed Guide ProgramsProceedings of the ACM on Programming Languages10.1145/36897488:OOPSLA2(1051-1080)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689748
DeYoung HMordido APfenning FDas A(2024)Parametric Subtyping for Structural Parametric PolymorphismProceedings of the ACM on Programming Languages10.1145/36329328:POPL(2700-2730)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632932

Index Terms

Parameterized Algebraic Protocols
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Abstract data types
        Data types and structures
        Polymorphism
        Recursion
      2. Language types
        Concurrent programming languages
        Functional languages

Recommendations

Gradually structured data

Dynamically-typed languages offer easy interaction with ad hoc data such as JSON and S-expressions; statically-typed languages offer powerful tools for working with structured data, notably algebraic datatypes, which are a core feature of typed languages ...
Manifest Contracts for Datatypes
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

We study algebraic data types in a manifest contract system, a software contract system where contract information occurs as refinement types. We first compare two simple approaches: refinements on type constructors and refinements on data constructors. ...
A decentralized analysis of multiparty protocols
Abstract
Protocols provide the unifying glue in concurrent and distributed software today; verifying that message-passing programs conform to such governing protocols is important but difficult. Static approaches based on multiparty session ...
Highlights
- A new analysis of multiparty protocols expressed as Multiparty Session Types (MPST).

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 7, Issue PLDI

June 2023

2020 pages

EISSN:2475-1421

DOI:10.1145/3554310

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2023 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 June 2023

Published in PACMPL Volume 7, Issue PLDI

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Fundação para a Ciência e a Tecnologia
COST (European Cooperation in Science and Technology)

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
334
Total Downloads

Downloads (Last 12 months)165
Downloads (Last 6 weeks)18

Reflects downloads up to 17 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ângelo PIgarashi AT. Vasconcelos V(2024)Linear Contextual Metaprogramming and Session TypesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.401.1401(1-10)Online publication date: 6-Apr-2024
https://doi.org/10.4204/EPTCS.401.1
Pham LWang DSaad FHoffmann J(2024)Programmable MCMC with Soundly Composed Guide ProgramsProceedings of the ACM on Programming Languages10.1145/36897488:OOPSLA2(1051-1080)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689748
DeYoung HMordido APfenning FDas A(2024)Parametric Subtyping for Structural Parametric PolymorphismProceedings of the ACM on Programming Languages10.1145/36329328:POPL(2700-2730)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632932

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents