Document Open Access Logo

Subtyping Context-Free Session Types

Authors Gil Silva , Andreia Mordido , Vasco T. Vasconcelos

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.11.pdf
  • Filesize: 1.22 MB
  • 19 pages

Document Identifiers

Author Details

Gil Silva
  • LASIGE, Faculdade de Ciências da Universidade de Lisboa, Portugal
Andreia Mordido
  • LASIGE, Faculdade de Ciências da Universidade de Lisboa, Portugal
Vasco T. Vasconcelos
  • LASIGE, Faculdade de Ciências da Universidade de Lisboa, Portugal

Funding

Support for this research was provided by the Fundação para a Ciência e a Tecnologia through project SafeSessions, ref. PTDC/CCI-COM/6453/2020, and by the LASIGE Research Unit, ref. UIDB/00408/2020 and ref. UIDP/00408/2020.

Acknowledgements

We thank Luca Padovani, Diana Costa, Diogo Poças and the anonymous reviewers for their insightful comments.

Cite AsGet BibTex

Gil Silva, Andreia Mordido, and Vasco T. Vasconcelos. Subtyping Context-Free Session Types. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CONCUR.2023.11

Abstract

Context-free session types describe structured patterns of communication on heterogeneously typed channels, allowing the specification of protocols unconstrained by tail recursion. The enhanced expressive power provided by non-regular recursion comes, however, at the cost of the decidability of subtyping, even if equivalence is still decidable. We present an approach to subtyping context-free session types based on a novel kind of observational preorder we call XYZW-simulation, which generalizes XY-simulation (also known as covariant-contravariant simulation) and therefore also bisimulation and plain simulation. We further propose a subtyping algorithm that we prove to be sound, and present an empirical evaluation in the context of a compiler for a programming language. Due to the general nature of the simulation relation upon which it is built, this algorithm may also find applications in other domains.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
  • Theory of computation → Concurrency
  • Software and its engineering → Concurrent programming structures
Keywords
  • Session types
  • Subtyping
  • Simulation
  • Simple grammars
  • Non-regular recursion

Metrics

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

Related Versions

References

  1. Fides Aarts and Frits W. Vaandrager. Learning I/O automata. In Paul Gastin and François 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 71-85. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_6.
  2. Bernardo Almeida, Andreia Mordido, Peter Thiemann, and Vasco T. Vasconcelos. Polymorphic lambda calculus with context-free session types. Inf. Comput., 289(Part):104948, 2022. URL: https://doi.org/10.1016/j.ic.2022.104948.
  3. Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconcelos. FreeST: Context-free session types in a functional language. In Francisco Martins and Dominic Orchard, editors, Proceedings Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES@ETAPS 2019, Prague, Czech Republic, 7th April 2019, volume 291 of EPTCS, pages 12-23, 2019. URL: https://doi.org/10.4204/EPTCS.291.2.
  4. Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconcelos. Deciding the bisimilarity of context-free session types. In TACAS@ 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II, volume 12079 of Lecture Notes in Computer Science, pages 39-56. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45237-7_3.
  5. Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconcelos. Kind inference for the FreeST programming language. CoRR, abs/2304.06396, 2023. URL: https://doi.org/10.48550/arXiv.2304.06396.
  6. Bernardo Almeida, Andreia Mordido, and Vasco Thudichum Vasconcelos. FreeST, a concurrent programming language with context-free session types, 2019. URL: https://freest-lang.github.io/.
  7. Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, and Moshe Y. Vardi. Alternating refinement relations. In Davide Sangiorgi and Robert de Simone, editors, CONCUR '98: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, Proceedings, volume 1466 of Lecture Notes in Computer Science, pages 163-178. Springer, 1998. URL: https://doi.org/10.1007/BFb0055622.
  8. Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575-631, 1993. URL: https://doi.org/10.1145/155183.155231.
  9. Jos C. M. Baeten, Jan A. Bergstra, and Jan Willem Klop. Decidability of bisimulation equivalence for processes generating context-free languages. J. ACM, 40(3):653-682, 1993. URL: https://doi.org/10.1145/174130.174141.
  10. Michael Brandt and Fritz Henglein. Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informaticae, 33(4):309-338, 1998. URL: https://doi.org/10.3233/FI-1998-33401.
  11. Olaf Burkart, Didier Caucal, and Bernhard Steffen. An elementary bisimulation decision procedure for arbitrary context-free processes. In Jirí Wiedermann and Petr Hájek, editors, Mathematical Foundations of Computer Science 1995, 20th International Symposium, MFCS'95, Prague, Czech Republic, August 28 - September 1, 1995, Proceedings, volume 969 of Lecture Notes in Computer Science, pages 423-433. Springer, 1995. URL: https://doi.org/10.1007/3-540-60246-1_148.
  12. Marco Carbone, Kohei Honda, and Nobuko Yoshida. Structured communication-centred programming for web services. In Rocco De Nicola, editor, Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings, volume 4421 of Lecture Notes in Computer Science, pages 2-17. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71316-6_2.
  13. Giuseppe Castagna and Alain Frisch. A gentle introduction to semantic subtyping. In Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 11-13 2005, Lisbon, Portugal, pages 198-199. ACM, 2005. URL: https://doi.org/10.1145/1069774.1069793.
  14. Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, and Luca Padovani. Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pages 5-17, 2014. URL: https://doi.org/10.1145/2535838.2535840.
  15. Koen Claessen and John Hughes. Quickcheck: a lightweight tool for random testing of Haskell programs. In Martin Odersky and Philip Wadler, editors, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montreal, Canada, September 18-21, 2000, pages 268-279. ACM, 2000. URL: https://doi.org/10.1145/351240.351266.
  16. Diana Costa, Andreia Mordido, Diogo Poças, and Vasco T. Vasconcelos. Higher-order context-free session types in system F. In Marco Carbone and Rumyana Neykova, editors, Proceedings of the 13th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES@ETAPS 2022, Munich, Germany, 3rd April 2022, volume 356 of EPTCS, pages 24-35, 2022. URL: https://doi.org/10.4204/EPTCS.356.3.
  17. Nils Anders Danielsson and Thorsten Altenkirch. Subtyping, declaratively. In 10th International Conference on Mathematics of Program Construction (MPC 2010), pages 100-118, Québec City, Canada, June 2010. Springer LNCS 6120. URL: https://doi.org/10.1007/978-3-642-13321-3_8.
  18. Ankush Das, Henry DeYoung, Andreia Mordido, and Frank Pfenning. Nested session types. In Nobuko Yoshida, editor, Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume 12648 of Lecture Notes in Computer Science, pages 178-206. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72019-3_7.
  19. Stephen Dolan. Algebraic Subtyping: Distinguished Dissertation 2017. BCS, Swindon, GBR, 2017. URL: https://www.cs.tufts.edu/~nr/cs257/archive/stephen-dolan/thesis.pdf.
  20. Ignacio Fábregas, David de Frutos-Escrig, and Miguel Palomino. Non-strongly stable orders also define interesting simulation relations. In Alexander Kurz, Marina Lenisa, and Andrzej Tarlecki, editors, Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings, volume 5728 of Lecture Notes in Computer Science, pages 221-235. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03741-2_16.
  21. Emily P. Friedman. The inclusion problem for simple languages. Theor. Comput. Sci., 1(4):297-316, 1976. URL: https://doi.org/10.1016/0304-3975(76)90074-8.
  22. Simon Gay. Subtyping between standard and linear function types. Technical report, University of Glasgow, 2006. Google Scholar
  23. Simon J. Gay. Bounded polymorphism in session types. Math. Struct. Comput. Sci., 18(5):895-930, 2008. URL: https://doi.org/10.1017/S0960129508006944.
  24. Simon J. Gay. Subtyping supports safe session substitution. In Sam Lindley, Conor McBride, Philip W. Trinder, and Donald 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 95-108. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_5.
  25. Simon J. Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Informatica, 42(2-3):191-225, 2005. URL: https://doi.org/10.1007/s00236-005-0177-z.
  26. Simon J. Gay and Vasco Thudichum Vasconcelos. Linear type theory for asynchronous session types. J. Funct. Program., 20(1):19-50, 2010. URL: https://doi.org/10.1017/S0956796809990268.
  27. Sheila A. Greibach. A new normal-form theorem for context-free phrase structure grammars. J. ACM, 12(1):42-52, 1965. URL: https://doi.org/10.1145/321250.321254.
  28. Jan Friso Groote and Hans Hüttel. Undecidable equivalences for basic process algebra. Inf. Comput., 115(2):354-371, 1994. URL: https://doi.org/10.1006/inco.1994.1101.
  29. Patrick Henry and Géraud Sénizergues. Lalblc a program testing the equivalence of dpda’s. In Stavros Konstantinidis, editor, Implementation and Application of Automata, pages 169-180, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  30. Yoram Hirshfeld, Mark Jerrum, and Faron Moller. A polynomial algorithm for deciding bisimilarity of normed context-free processes. Theor. Comput. Sci., 158(1&2):143-159, 1996. URL: https://doi.org/10.1016/0304-3975(95)00064-X.
  31. Kohei Honda. Types for dyadic interaction. In Eike 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. URL: https://doi.org/10.1007/3-540-57208-2_35.
  32. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Hankin, editor, Programming Languages and Systems - ESOP'98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, volume 1381 of Lecture Notes in Computer Science, pages 122-138. Springer, 1998. URL: https://doi.org/10.1007/BFb0053567.
  33. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In George C. Necula and Philip Wadler, editors, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 273-284. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328472.
  34. Ross Horne and Luca Padovani. A logical account of subtyping for session types. CoRR, abs/2304.06398, 2023. URL: https://doi.org/10.48550/arXiv.2304.06398.
  35. Petr Jancar and Faron Moller. Techniques for decidability and undecidability of bisimilarity. In Jos C. M. Baeten and Sjouke Mauw, editors, CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings, volume 1664 of Lecture Notes in Computer Science, pages 30-45. Springer, 1999. URL: https://doi.org/10.1007/3-540-48320-9_5.
  36. A. J. Korenjak and John E. Hopcroft. Simple deterministic languages. In 7th Annual Symposium on Switching and Automata Theory, Berkeley, California, USA, October 23-25, 1966, pages 36-46. IEEE Computer Society, 1966. URL: https://doi.org/10.1109/SWAT.1966.22.
  37. Zeeshan Lakhani, Ankush Das, Henry DeYoung, Andreia Mordido, and Frank Pfenning. Polarized subtyping. In Programming Languages and Systems: 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, pages 431-461. Springer International Publishing Cham, 2022. Google Scholar
  38. Kim Guldstrand Larsen and Bent Thomsen. A modal process logic. In Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), Edinburgh, Scotland, UK, July 5-8, 1988, pages 203-210. IEEE Computer Society, 1988. URL: https://doi.org/10.1109/LICS.1988.5119.
  39. Barbara Liskov. Keynote address - data abstraction and hierarchy. In Leigh R. Power and Zvi Weiss, editors, Addendum to the Proceedings on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 1987 Addendum, Orlando, Florida, USA, October 4-8, 1987, pages 17-34. ACM, 1987. URL: https://doi.org/10.1145/62138.62141.
  40. Karl Mazurak, Jianzhou Zhao, and Steve Zdancewic. Lightweight linear types in System F^∘. In Andrew Kennedy and Nick Benton, editors, Proceedings of TLDI 2010: 2010 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Madrid, Spain, January 23, 2010, pages 77-88. ACM, 2010. URL: https://doi.org/10.1145/1708016.1708027.
  41. Robin Milner. An algebraic definition of simulation between programs. In D. C. Cooper, editor, Proceedings of the 2nd International Joint Conference on Artificial Intelligence. London, UK, September 1-3, 1971, pages 481-489. William Kaufmann, 1971. URL: http://ijcai.org/Proceedings/71/Papers/044.pdf.
  42. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. URL: https://doi.org/10.1007/3-540-10235-3.
  43. Luca Padovani. Context-free session type inference. ACM Trans. Program. Lang. Syst., 41(2):9:1-9:37, 2019. URL: https://doi.org/10.1145/3229062.
  44. David Michael Ritchie Park. Concurrency and automata on infinite sequences. In Peter Deussen, editor, Theoretical Computer Science, 5th GI-Conference, Karlsruhe, Germany, March 23-25, 1981, Proceedings, volume 104 of Lecture Notes in Computer Science, pages 167-183. Springer, 1981. URL: https://doi.org/10.1007/BFb0017309.
  45. Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. Google Scholar
  46. Benjamin C. Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. Math. Struct. Comput. Sci., 6(5):409-453, 1996. URL: https://doi.org/10.1017/s096012950007002x.
  47. Diogo Poças, Diana Costa, Andreia Mordido, and Vasco T. Vasconcelos. System F^μ_ω with context-free session types. In Thomas Wies, editor, 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, Paris, France, April 22-27, 2023, Proceedings, volume 13990 of Lecture Notes in Computer Science, pages 392-420. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30044-8_15.
  48. Davide Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2011. URL: https://doi.org/10.1017/CBO9780511777110.
  49. Gil Silva, Andreia Mordido, and Vasco T. Vasconcelos. Subtyping context-free session types. CoRR, abs/2307.05661, 2023. URL: https://doi.org/10.48550/arXiv.2307.05661.
  50. Kaku Takeuchi, Kohei Honda, and Makoto Kubo. An interaction-based language and its typing system. In Constantine Halatsis, Dimitris G. Maritsas, George Philokyprou, and Sergios 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. URL: https://doi.org/10.1007/3-540-58184-7_118.
  51. Peter Thiemann and Vasco T. Vasconcelos. Context-free session types. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 462-475. ACM, 2016. URL: https://doi.org/10.1145/2951913.2951926.
  52. Rob J. van Glabbeek. The linear time - branching time spectrum II. In Eike 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 66-81. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_6.
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 Imprint Privacy Contact