Document Open Access Logo

Session Types with Arithmetic Refinements

Authors Ankush Das , Frank Pfenning

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.13.pdf
  • Filesize: 0.48 MB
  • 18 pages

Document Identifiers

Author Details

Ankush Das
  • Carnegie Mellon University, Pittsburgh, PA, USA
Frank Pfenning
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

  • Das, Ankush: funded by the National Science Foundation under SaTC Award 1801369 and CAREER Award 1845514.
  • Pfenning, Frank: funded by the National Science Foundation under Grant No. 1718276.

Cite As Get BibTex

Ankush Das and Frank Pfenning. Session Types with Arithmetic Refinements. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CONCUR.2020.13

Abstract

Session types statically prescribe bidirectional communication protocols for message-passing processes. However, simple session types cannot specify properties beyond the type of exchanged messages. In this paper we extend the type system by using index refinements from linear arithmetic capturing intrinsic attributes of data structures and algorithms. We show that, despite the decidability of Presburger arithmetic, type equality and therefore also subtyping and type checking are now undecidable, which stands in contrast to analogous dependent refinement type systems from functional languages. We also present a practical, but incomplete algorithm for type equality, which we have used in our implementation of Rast, a concurrent session-typed language with arithmetic index refinements as well as ergometric and temporal types. Moreover, if necessary, the programmer can propose additional type bisimulations that are smoothly integrated into the type equality algorithm.

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
  • Theory of computation → Linear logic
  • Theory of computation → Logic and verification
  • Computing methodologies → Concurrent programming languages
  • Theory of computation → Type theory
Keywords
  • Session Types
  • Refinement Types
  • Type Equality

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconcelos. Deciding the bisimilarity of context-free session types. In A. Biere and D. Parker, editors, 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), pages 39-56, Dublin, Ireland, April 2020. Springer LNCS 12079. Google Scholar
  2. Pedro Baltazar, Dimitris Mostrous, and Vasco T. Vasconcelos. Linearly refined session types. In S. Alves and I. Mackie, editors, International Workshop on Linearity (LINEARITY 2012), pages 38-49, Tallinn, Estonia, April 2012. EPTCS 101. Google Scholar
  3. Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models. In L. Pacholski and J. Tiuryn, editors, Selected Papers from the 8th International Workshop on Computer Science Logic (CSL 1994), pages 121-135, Kazimierz, Poland, September 1994. Springer LNCS 933. An extended version appears as Technical Report UCAM-CL-TR-352, University of Cambridge. Google Scholar
  4. Laura Bocchi, Kohei Honda, Emilio Tuosto, and Nobuko Yoshida. A theory of design-by-contract for distributed multiparty interactions. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, pages 162-176, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  5. Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. A sound algorithm for asynchronous session subtyping. In W. Fokkink and R. van Glabbeek, editors, 30th International Conference on Concurrency Theory (CONCUR 2019), pages 38:1-38:16, Amsterdam, The Netherlands, August 2019. LIPIcs 140. Google Scholar
  6. Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. Undecidability of asynchronous session subtyping. Information & Computation, 256:300-320, 2017. Google Scholar
  7. Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho. Behavioral polymorphism and parametricity in session-based communication. In M.Felleisen and P.Gardner, editors, Proceedings of the European Symposium on Programming (ESOP'13), pages 330-349, Rome, Italy, March 2013. Springer LNCS 7792. Google Scholar
  8. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In P.Gastin and F.Laroussinie, editors, Proceedings of the 21st International Conference on Concurrency Theory (CONCUR 2010), pages 222-236, Paris, France, August 2010. Springer LNCS 6269. Google Scholar
  9. Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Mathematical Structures in Computer Science, 26(3):367-423, 2016. Special Issue on Behavioural Types. Google Scholar
  10. David C. Cooper. Theorem proving in arithmetic without multiplication. Machine Intelligence, 7:91-99, 1972. Google Scholar
  11. Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, and Ishani Santurkar. Resource-aware session types for digital contracts, 2019. URL: http://arxiv.org/abs/1902.06056.
  12. Ankush Das, Jan Hoffmann, and Frank Pfenning. Parallel complexity analysis with temporal session types. In M. Flatt, editor, Proceedings of International Conference on Functional Programming (ICFP 2018), pages 91:1-91:30, St. Louis, Missouri, USA, September 2018. ACM. Google Scholar
  13. Ankush Das, Jan Hoffmann, and Frank Pfenning. Work analysis with resource-aware session types. In A. Dawar and E. Grädel, editors, Proceedings of 33rd Symposium on Logic in Computer Science (LICS'18), pages 305-314, Oxford, UK, July 2018. Google Scholar
  14. Ankush Das and Frank Pfenning. Rast: Resource-aware session types with arithmetic refinements. In Z. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), pages 4:1-4:17. LIPIcs 167, June 2020. System description. To appear. Google Scholar
  15. Farzaneh Derakhshan and Frank Pfenning. Circular proofs as session-typed processes: A local validity condition, August 2019. URL: http://arxiv.org/abs/1908.01909.
  16. Juliana Franco and Vasco T. Vasconcelos. A concurrent programming language with refined session types. In S. Counsell and M. Núñez, editors, Software Engineering and Formal Methods (SEFM 2013), pages 15-28, Madrid, Spain, September 2013. Springer LNCS 8368. Google Scholar
  17. Simon J. Gay and Malcolm Hole. Subtyping for session types in the π-calculus. Acta Informatica, 42(2-3):191-225, 2005. Google Scholar
  18. Simon J. Gay and Vasco T. Vasconcelos. Linear type theory for asynchronous session types. Journal of Functional Programming, 20(1):19-50, January 2010. Google Scholar
  19. Hannah Gommerstadt. Session-Typed Concurrent Contracts. PhD thesis, Carnegie Mellon University, September 2019. Available as Technical Report CMU-CS-19-119. Google Scholar
  20. Hannah Gommerstadt, Limin Jia, and Frank Pfenning. Session-typed concurrent contracts. In A. Ahmed, editor, European Symposium on Programming (ESOP'18), pages 771-798, Thessaloniki, Greece, April 2018. Springer LNCS 10801. Google Scholar
  21. Dennis Griffith. Polarized Substructural Session Types. PhD thesis, University of Illinois at Urbana-Champaign, April 2016. Google Scholar
  22. Dennis Griffith and Elsa L. Gunter. LiquidPi: Inferrable dependent session types. In Proceedings of the NASA Formal Methods Symposium, pages 186-197. Springer LNCS 7871, 2013. Google Scholar
  23. Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers. Actris: Session-type based reasoning in separation logic. Proc. ACM Program. Lang., 4(POPL), December 2019. URL: https://doi.org/10.1145/3371074.
  24. Kohei Honda. Types for dyadic interaction. In E. Best, editor, 4th International Conference on Concurrency Theory (CONCUR 1993), pages 509-523. Springer LNCS 715, 1993. Google Scholar
  25. Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In C. Hankin, editor, 7th European Symposium on Programming Languages and Systems (ESOP 1998), pages 122-138. Springer LNCS 1381, 1998. Google Scholar
  26. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In G. Necula and P. Wadler, editors, Proceedings of the 35th Symposium on Principles of Programming Language (POPL 2008), pages 273-284, San Francisco, California, USA, January 2008. ACM. Google Scholar
  27. Julien Lange and Nobuko Yoshida. On the undecidability of asynchronous session subtyping. In Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), pages 441-457. Springer LNCS 10203, 2017. Google Scholar
  28. Sam Lindley and J. Garrett Morris. Talking bananas: Structural recursion for session types. In J. Garrigue, G. Keller, and E. Sumii, editors, Proceedings of the 21st International Conference on Functional Programming, pages 434-447, Nara, Japan, September 2016. ACM. Google Scholar
  29. Bertrand Meyer. Applying “design by contract”. Computer, 25(10):40–51, October 1992. URL: https://doi.org/10.1109/2.161279.
  30. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., USA, 1967. Google Scholar
  31. Dimitris Mostrous and Nobuko Yoshida. Session typing and asynchronous subtyping for the higher-order π-calculus. Information & Computation, 241:227-263, 2015. Google Scholar
  32. Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades, III. Quantitative program reasoning with graded modal types. In International Conference on Functional Programming (ICFP 2019), pages 110:1-110:30, Berlin, Germany, August 2019. ACM. Google Scholar
  33. Frank Pfenning, Luís Caires, and Bernardo Toninho. Proof-carrying code in a session-typed process calculus. In 1st International Conference on Certified Programs and Proofs (CPP 2011), pages 21-36, Kenting, Taiwan, December 2011. Springer LNCS 7086. Google Scholar
  34. Frank Pfenning and Dennis Griffith. Polarized substructural session types. In A. Pitts, editor, Proceedings of the 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015), pages 3-22, London, England, April 2015. Springer LNCS 9034. Invited talk. Google Scholar
  35. Klaas Pruiksma and Frank Pfenning. A message-passing interpretation of adjoint logic. In F. Martins and D. Orchard, editors, Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software (PLACES 2019), pages 60-79, Prague, Czech Republic, April 2019. EPTCS 291. Google Scholar
  36. Rast language, February 2020. Version 1.01. URL: https://bitbucket.org/fpfenning/rast/src/master/rast/.
  37. Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala. Liquid types. In R. Gupta and S. Amarasinghe, editors, Conference on Programming Language Design and Implementation (PLDI 2008), pages 159-169, Tuscon, Arizona, June 2008. ACM. Google Scholar
  38. Peter Thiemann and Vasco T. Vasconcelos. Context-free session types. In Proceedings of the 21st International Conference on Functional Programming (ICFP 2016), pages 462-475, Nara, Japan, September 2016. ACM. Google Scholar
  39. Peter Thiemann and Vasco T. Vasconcelos. Label-dependent session types. In L. Birkedal, editor, Proceedings of the Symposium on Programming Languages (POPL 2020), pages 67:1-67:29, New Orleans, Louisiana, USA, January 2020. ACM Proceedings on Programming Languages 4. Google Scholar
  40. Bernardo Toninho, Luís Caires, and Frank Pfenning. Dependent session types via intuitionistic linear type theory. In P.Schneider-Kamp and M.Hanus, editors, Proceedings of the 13th International Conference on Principles and Practice of Declarative Programming (PPDP 2011), pages 161-172, Odense, Denmark, July 2011. ACM. Google Scholar
  41. Bernardo Toninho and Nobuko Yoshida. Depending on session-types processes. In C. Baier and U. Dal Lago, editors, 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018), pages 128-145, Thessaloniki, Greece, April 2018. Springer LNCS 10803. Google Scholar
  42. Vasco T. Vasconcelos. Fundamentals of session types. Information & Computation, 217:52-70, 2012. Google Scholar
  43. Philip Wadler. Propositions as sessions. In Proceedings of the 17th International Conference on Functional Programming (ICFP 2012), pages 273-286, Copenhagen, Denmark, September 2012. ACM Press. Google Scholar
  44. Hanwen Wu and Hongwei Xi. Dependent session types, 2017. URL: http://arxiv.org/abs/1704.07004.
  45. Hongwei Xi. Applied type system: Extended abstract. In S. Berardi, M. Coppo, and F. Damiani, editors, International Workshop on Types for Proofs and Programming (TYPES 2003), pages 394-408, Torino, Italy, April 2003. Springer LNCS 3085. Google Scholar
  46. Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In A. Aiken, editor, Conference Record of the 26th Symposium on Principles of Programming Languages (POPL 1999), pages 214-227, San Antonio, Texas, USA, January 1999. ACM Press. Google Scholar
  47. Christoph Zenger. Indexed types. Theoretical Computer Science, 187:147-165, 1997. Google Scholar
  48. Fangyi Zhou. Refinement session types. Master’s thesis, Imperial College London, 2019. Google Scholar
  49. Fangyi Zhou, Francisco Ferreira, Rumyana Neykova, and Nobuko Yoshida. Fluid Types: Statically Verified Distributed Protocols with Refinements. In 11th Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software, 2019. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact