research-article

Talking bananas: structural recursion for session types

Authors:

J. Garrett MorrisAuthors Info & Claims

ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

Pages 434 - 447

https://doi.org/10.1145/2951913.2951921

Published: 04 September 2016 Publication History

Abstract

Session types provide static guarantees that concurrent programs respect communication protocols. We give a novel account of recursive session types in the context of GV, a small concurrent extension of the linear λ-calculus. We extend GV with recursive types and catamorphisms, following the initial algebra semantics of recursion, and show that doing so naturally gives rise to recursive session types. We show that this principled approach to recursion resolves long-standing problems in the treatment of duality for recursive session types.

We characterize the expressiveness of GV concurrency by giving a CPS translation to (non-concurrent) λ-calculus and proving that reduction in GV is simulated by full reduction in λ-calculus. This shows that GV remains terminating in the presence of positive recursive types, and that such arguments extend to other extensions of GV, such as polymorphism or non-linear types, by appeal to normalization results for sequential λ-calculi. We also show that GV remains deadlock free and deterministic in the presence of recursive types.

Finally, we extend CP, a session-typed process calculus based on linear logic, with recursive types, and show that doing so preserves the connection between reduction in GV and cut elimination in CP.

References

[1]

S. Abramsky. Proofs as processes. Theor. Comput. Sci., 135(1):5–9, 1994.

Digital Library

[2]

R. Atkey, S. Lindley, and J. G. Morris. Conflation confers concurrency. In S. Lindley, C. McBride, P. W. Trinder, and D. Sannella, editors, A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, volume 9600 of Lecture Notes in Computer Science, pages 32–55. Springer, 2016.

[3]

D. Baelde. Least and greatest fixed points in linear logic. ACM Trans. Comput. Logic, 13(1):2:1–2:44, Jan. 2012.

Digital Library

[4]

D. Baelde and D. Miller. Least and greatest fixed points in linear logic. In N. Dershowitz and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings, volume 4790 of Lecture Notes in Computer Science, pages 92–106. Springer, 2007.

Digital Library

[5]

G. Bellin and P. J. Scott. On the π-Calculus and linear logic. Theoretical Computer Science, 135(1):11–65, 1994.

Digital Library

[6]

G. Bernardi and M. Hennessy. Using higher-order contracts to model session types (extended abstract). In P. Baldan and D. Gorla, editors, CONCUR 2014, volume 8704 of Lecture Notes in Computer Science, pages 387–401. Springer, 2014.

[7]

G. Bernardi and M. Hennessy. Using higher-order contracts to model session types. CoRR, abs/1310.6176v4, 2015.

[8]

G. Bernardi, O. Dardha, S. J. Gay, and D. Kouzapas. On duality relations for session types. In Trustworthy Global Computing - 9th International Symposium, TGC 2014, Rome, Italy, September 5-6, 2014. Revised Selected Papers, pages 51–66, 2014.

[9]

R. S. Bird and O. de Moor. Algebra of programming. Prentice Hall International series in computer science. Prentice Hall, 1997.

Digital Library

[10]

V. Bono and L. Padovani. Typing copyless message passing. Logical Methods in Computer Science, 8(1), 2012.

[11]

V. Bono, L. Padovani, and A. Tosatto. Polymorphic types for leak detection in a session-oriented functional language. In D. Beyer and M. Boreale, editors, Formal Techniques for Distributed Systems - Joint IFIP WG 6.1 International Conference, FMOODS/FORTE 2013, Held as Part of the 8th International Federated Conference on Distributed Computing Techniques, DisCoTec 2013, Florence, Italy, June 3-5, 2013. Proceedings, volume 7892 of Lecture Notes in Computer Science, pages 83–98. Springer, 2013.

[12]

M. Boreale. On the expressiveness of internal mobility in namepassing calculi. In U. Montanari and V. Sassone, editors, CONCUR ’96, Concurrency Theory, 7th International Conference, Pisa, Italy, August 26-29, 1996, Proceedings, volume 1119 of Lecture Notes in Computer Science, pages 163–178. Springer, 1996.

Digital Library

[13]

L. Caires and F. Pfenning. Session types as intuitionistic linear propositions. In P. Gastin and F. Laroussinie, editors, CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, volume 6269 of Lecture Notes in Computer Science, pages 222–236. Springer, 2010.

Digital Library

[14]

M. Carbone, S. Lindley, F. Montesi, C. Shürmann, and P. Wadler. Coherence generalises duality: a logical explanation of multiparty session types. In CONCUR. LIPICS, 2016. To appear.

[15]

O. Danvy and L. R. Nielsen. A first-order one-pass CPS transformation. In M. Nielsen and U. Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, volume 2303 of Lecture Notes in Computer Science, pages 98–113. Springer, 2002.

Digital Library

[16]

O. Dardha. Recursive session types revisited. In Proceedings Third Workshop on Behavioural Types, BEAT 2014, Rome, Italy, 1st September 2014.

[17]

, pages 27–34, 2014.

[18]

O. Dardha, E. Giachino, and D. Sangiorgi. Session types revisited. In D. D. Schreye, G. Janssens, and A. King, editors, Principles and Practice of Declarative Programming, PPDP’12, Leuven, Belgium - September 19 - 21, 2012, pages 139–150. ACM, 2012.

Digital Library

[19]

A. Filinski. Linear continuations. In R. Sethi, editor, Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 19-22, 1992, pages 27–38. ACM Press, 1992.

Digital Library

[20]

P. Freyd. Algebraically complete categories. In G. R. Aurelio Carboni, Maria Cristina Pedicchio, editor, Category Theory - Proceedings of the International Conference held in Como, Italy, July 22–28, 1990. Springer, 1990.

[21]

S. J. Gay and V. T. Vasconcelos. Linear type theory for asynchronous session types. Journal of Functional Programming, 20(01):19–50, 2010.

Digital Library

[22]

J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Initial algebra semantics and continuous algebras. J. ACM, 24(1):68–95, 1977.

Digital Library

[23]

K. Honda. Types for dyadic interaction. In E. Best, editor, CONCUR ’93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, volume 715 of Lecture Notes in Computer Science, pages 509–523. Springer, 1993.

Digital Library

[24]

K. Honda, V. T. Vasconcelos, and M. Kubo. Language primitives and type discipline for structured communication-based programming. In C. Hankin, editor, ESOP, volume 1381 of Lecture Notes in Computer Science, pages 122–138. Springer, 1998.

Digital Library

[25]

N. Kobayashi, B. C. Pierce, and D. N. Turner. Linearity and the picalculus. ACM Trans. Program. Lang. Syst., 21(5):914–947, 1999.

Digital Library

[26]

J. Lévy and L. Maranget. Explicit substitutions and programming languages. In Foundations of Software Technology and Theoretical Computer Science, 1999, volume 1738 of LNCS. Springer, 1999.

Digital Library

[27]

S. Lindley and J. G. Morris. A semantics for propositions as sessions. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, pages 560–584, 2015.

[28]

S. Lindley and J. G. Morris. Lightweight functional session types, 2015.

[29]

Draft http://homepages.inf.ed.ac.uk/slindley/ papers/fst-draft-february2015.pdf.

[30]

B. Liskov and L. Shrira. Promises: Linguistic support for efficient asynchronous procedure calls in distributed systems. In Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, PLDI ’88, pages 260–267, New York, NY, USA, 1988. ACM.

Digital Library

[31]

E. Meijer, M. M. Fokkinga, and R. Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In J. Hughes, editor, Functional Programming Languages and Computer Architecture, 5th ACM Conference, Cambridge, MA, USA, August 26-30, 1991, Proceedings, volume 523 of Lecture Notes in Computer Science, pages 124–144. Springer, 1991.

Digital Library

[32]

K. Takeuchi, K. Honda, and M. Kubo. An interaction-based language and its typing system. In C. Halatsis, D. G. Maritsas, G. Philokyprou, and S. Theodoridis, editors, PARLE ’94: Parallel Architectures and Languages Europe, 6th International PARLE Conference, Athens, Greece, July 4-8, 1994, Proceedings, volume 817 of Lecture Notes in Computer Science, pages 398–413. Springer, 1994.

Digital Library

[33]

The Links Team. Links, 2016. http://groups.inf.ed.ac.uk/ links.

[34]

B. Toninho, L. Caires, and F. Pfenning. Corecursion and nondivergence in session-typed processes. In Trustworthy Global Computing - 9th International Symposium, TGC 2014, Rome, Italy, September 5-6, 2014. Revised Selected Papers, pages 159–175, 2014.

[35]

V. T. Vasconcelos, S. J. Gay, and A. Ravara. Type checking a multithreaded functional language with session types. Theor. Comput. Sci., 368(1-2):64–87, 2006.

Digital Library

[36]

P. Wadler. Propositions as sessions. J. Funct. Program., 24(2-3):384– 418, 2014.

Cited By

Cavoj SNikitin IPerkins CDardha O(2024)Session Types for the Transport Layer: Towards an Implementation of TCPElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.401.3401(22-36)Online publication date: 6-Apr-2024
https://doi.org/10.4204/EPTCS.401.3
Dal Lago UPadovani L(2024)On the Almost-Sure Termination of Binary SessionsProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678239(1-12)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678239
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
Show More Cited By

Index Terms

Talking bananas: structural recursion for session types
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
      2. Language types

Recommendations

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 ...
Talking bananas: structural recursion for session types
ICFP '16

Session types provide static guarantees that concurrent programs respect communication protocols. We give a novel account of recursive session types in the context of GV, a small concurrent extension of the linear λ-calculus. We extend GV with ...
Acyclic Recursion with Polymorphic Types and Underpecification
ICAART 2016: Proceedings of the 8th International Conference on Agents and Artificial Intelligence

The paper extends Moschovakis higher-order type theory of acyclic recursion by adding type polymorphism. We extend the type system of the theory to model parametric information that pertains to underspecified types. Different kinds of type polymorphism ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

September 2016

501 pages

ISBN:9781450342193

DOI:10.1145/2951913

General Chairs:
Jacques Garrigue
Nagoya University, Japan
,
Gabriele Keller
University of New South Wales, Australia
,
Program Chair:
Eijiro Sumii
Tohoku University, Japan

ACM SIGPLAN Notices Volume 51, Issue 9
ICFP '16
September 2016
501 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/3022670
Editor:
Matthew Fluet
Issue’s Table of Contents

Copyright © 2016 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].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 September 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Engineering and Physical Sciences Research Council

Conference

ICFP'16

Sponsor:

SIGPLAN

ICFP'16: ACM SIGPLAN International Conference on Functional Programming

September 18 - 24, 2016

Nara, Japan

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

42
Total Citations
View Citations
427
Total Downloads

Downloads (Last 12 months)20
Downloads (Last 6 weeks)3

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Cavoj SNikitin IPerkins CDardha O(2024)Session Types for the Transport Layer: Towards an Implementation of TCPElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.401.3401(22-36)Online publication date: 6-Apr-2024
https://doi.org/10.4204/EPTCS.401.3
Dal Lago UPadovani L(2024)On the Almost-Sure Termination of Binary SessionsProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678239(1-12)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678239
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
Jacobs JHinrichsen JKrebbers R(2024)Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message PassingProceedings of the ACM on Programming Languages10.1145/36328898:POPL(1385-1417)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632889
Horne RPadovani L(2023)A Logical Account of Subtyping for Session TypesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.378.3378(26-37)Online publication date: 13-Apr-2023
https://doi.org/10.4204/EPTCS.378.3
Mordido ASpaderna JThiemann PVasconcelos V(2023)Parameterized Algebraic ProtocolsProceedings of the ACM on Programming Languages10.1145/35912777:PLDI(1389-1413)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591277
Jacobs JBalzer S(2023)Higher-Order Leak and Deadlock Free LocksProceedings of the ACM on Programming Languages10.1145/35712297:POPL(1027-1057)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571229
Poças DCosta DMordido AVasconcelos V(2023)System with Context-free Session TypesProgramming Languages and Systems10.1007/978-3-031-30044-8_15(392-420)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_15
Jacobs JBalzer SKrebbers R(2022)Multiparty GV: functional multiparty session types with certified deadlock freedomProceedings of the ACM on Programming Languages10.1145/35476386:ICFP(466-495)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547638
Das ADeyoung HMordido APfenning F(2022)Nested Session TypesACM Transactions on Programming Languages and Systems10.1145/353965644:3(1-45)Online publication date: 15-Jul-2022
https://dl.acm.org/doi/10.1145/3539656
Show More Cited By

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents