Document Open Access Logo

Inference Systems with Corules for Fair Subtyping and Liveness Properties of Binary Session Types

Authors Luca Ciccone , Luca Padovani

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2021.125.pdf
  • Filesize: 0.7 MB
  • 16 pages

Document Identifiers

Author Details

Luca Ciccone
  • University of Torino, Italy
Luca Padovani
  • University of Torino, Italy

Acknowledgements

We are grateful to Francesco Dagnino for his feedback on an early version of this paper. The anonymous ICALP reviewers provided useful comments and suggestions that helped us improving the paper.

Cite As Get BibTex

Luca Ciccone and Luca Padovani. Inference Systems with Corules for Fair Subtyping and Liveness Properties of Binary Session Types. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 125:1-125:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ICALP.2021.125

Abstract

Many properties of communication protocols stem from the combination of safety and liveness properties. Characterizing such combined properties by means of a single inference system is difficult because of the fundamentally different techniques (coinduction and induction, respectively) usually involved in defining and proving them. In this paper we show that Generalized Inference Systems allow for simple and insightful characterizations of (at least some of) these combined inductive/coinductive properties for dependent session types. In particular, we illustrate the role of corules in characterizing weak termination (the property of protocols that can always eventually terminate), fair compliance (the property of interactions that can always be extended to reach client satisfaction) and also fair subtyping, a liveness-preserving refinement relation for session types.

Subject Classification

ACM Subject Classification
  • Theory of computation → Axiomatic semantics
  • Theory of computation → Type structures
  • Theory of computation → Program specifications
Keywords
  • Inference systems
  • session types
  • safety
  • liveness
  • induction
  • coinduction

Metrics

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

Supplementary Materials

References

  1. Peter Aczel. An introduction to inductive definitions. In Jon Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 739-782. Elsevier, 1977. URL: https://doi.org/10.1016/S0049-237X(08)71120-0.
  2. Bowen Alpern and Fred B. Schneider. Defining liveness. Inf. Process. Lett., 21(4):181-185, 1985. URL: https://doi.org/10.1016/0020-0190(85)90056-0.
  3. Bowen Alpern and Fred B. Schneider. Recognizing safety and liveness. Distributed Comput., 2(3):117-126, 1987. URL: https://doi.org/10.1007/BF01782772.
  4. Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. Behavioral types in programming languages. Found. Trends Program. Lang., 3(2-3):95-230, 2016. URL: https://doi.org/10.1561/2500000031.
  5. Davide Ancona, Francesco Dagnino, and Elena Zucca. Generalizing inference systems by coaxioms. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10201 of Lecture Notes in Computer Science, pages 29-55. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_2.
  6. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  7. Giovanni Bernardi and Matthew Hennessy. Using higher-order contracts to model session types. Log. Methods Comput. Sci., 12(2), 2016. URL: https://doi.org/10.2168/LMCS-12(2:10)2016.
  8. Julian C. Bradfield and Colin Stirling. Modal mu-calculi. In Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning, pages 721-756. North-Holland, 2007. URL: https://doi.org/10.1016/s1570-2464(07)80015-2.
  9. Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Elena Giachino, and Luca Padovani. Foundations of session types. In António Porto and Francisco Javier López-Fraguas, editors, Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal, pages 219-230. ACM, 2009. URL: https://doi.org/10.1145/1599410.1599437.
  10. Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Elena Giachino, and Luca Padovani. Foundations of session types: 10 years later. In Ekaterina Komendantskaya, editor, Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019, Porto, Portugal, October 7-9, 2019, pages 1:1-1:3. ACM, 2019. URL: https://doi.org/10.1145/3354166.3356340.
  11. Luca Ciccone. Flexible coinduction in agda. Master’s thesis, DIBRIS, Università di Genova, Italy, 2020. URL: http://arxiv.org/abs/2002.06047.
  12. Luca Ciccone, Francesco Dagnino, and Elena Zucca. Flexible coinduction in Agda. In Schloss Dagstuhl Leibniz-Zentrum für Informatik, editor, Proceedings of the 12th conference on Interactive Theorem Proving, ITP 2021, 2021. to appear. Google Scholar
  13. Luca Ciccone, Francesco Dagnino, and Elena Zucca. Inference Systems in Agda, 2021. URL: https://github.com/LcicC/inference-systems-agda [cited Feb 1, 2021].
  14. Luca Ciccone and Luca Padovani. A Dependently Typed Linear π-Calculus in Agda. In PPDP'20: 22nd International Symposium on Principles and Practice of Declarative Programming, Bologna, Italy, 9-10 September, 2020, pages 8:1-8:14. ACM, 2020. URL: https://doi.org/10.1145/3414080.3414109.
  15. Luca Ciccone and Luca Padovani. Fair Subtyping in Agda, 2021. URL: https://github.com/boystrange/FairSubtypingAgda/tree/v1.0 [cited May 1, 2021].
  16. Francesco Dagnino. Coaxioms: flexible coinductive definitions by inference systems. Log. Methods Comput. Sci., 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:26)2019.
  17. Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. J. ACM, 55(4):19:1-19:64, 2008. URL: https://doi.org/10.1145/1391289.1391293.
  18. 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.
  19. 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.
  20. Matthew Hennessy. Algebraic theory of processes. MIT Press series in the foundations of computing. MIT Press, 1988. Google Scholar
  21. 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.
  22. 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.
  23. Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of session types and behavioural contracts. ACM Comput. Surv., 49(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2873052.
  24. Dexter Kozen. Results on the propositional mu-calculus. Theor. Comput. Sci., 27:333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  25. Maurizio Murgia. A note on compliance relations and fixed points. In Massimo Bartoletti, Ludovic Henrio, Anastasia Mavridou, and Alceste Scalas, editors, Proceedings 12th Interaction and Concurrency Experience, ICE 2019, Copenhagen, Denmark, 20-21 June 2019, volume 304 of EPTCS, pages 38-47, 2019. URL: https://doi.org/10.4204/EPTCS.304.3.
  26. Rocco De Nicola and Matthew Hennessy. Testing equivalences for processes. Theor. Comput. Sci., 34:83-133, 1984. URL: https://doi.org/10.1016/0304-3975(84)90113-0.
  27. Ulf Norell. Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden., 2007. URL: http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf.
  28. Susan S. Owicki and Leslie Lamport. Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst., 4(3):455-495, 1982. URL: https://doi.org/10.1145/357172.357178.
  29. Luca Padovani. Fair subtyping for open session types. In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, pages 373-384. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_34.
  30. Luca Padovani. Fair subtyping for multi-party session types. Math. Struct. Comput. Sci., 26(3):424-464, 2016. URL: https://doi.org/10.1017/S096012951400022X.
  31. Arend Rensink and Walter Vogler. Fair testing. Inf. Comput., 205(2):125-198, 2007. URL: https://doi.org/10.1016/j.ic.2006.06.002.
  32. Peter Thiemann and Vasco T. Vasconcelos. Label-dependent session types. Proc. ACM Program. Lang., 4(POPL):67:1-67:29, 2020. URL: https://doi.org/10.1145/3371135.
  33. Bernardo Toninho, Luís Caires, and Frank Pfenning. Dependent session types via intuitionistic linear type theory. In Peter Schneider-Kamp and Michael Hanus, editors, Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 20-22, 2011, Odense, Denmark, pages 161-172. ACM, 2011. URL: https://doi.org/10.1145/2003476.2003499.
  34. Bernardo Toninho and Nobuko Yoshida. Depending on session-typed processes. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10803 of Lecture Notes in Computer Science, pages 128-145. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_7.
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