Document Open Access Logo

Around Classical and Intuitionistic Linear Processes

Authors Juan C. Jaramillo , Dan Frumin , Jorge A. Pérez

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.30.pdf
  • Filesize: 0.93 MB
  • 19 pages

Document Identifiers

Author Details

Juan C. Jaramillo
  • Unversity of Groningen, The Netherlands
Dan Frumin
  • Unversity of Groningen, The Netherlands
Jorge A. Pérez
  • Unversity of Groningen, The Netherlands

Funding

  • Jaramillo, Juan C.: Ministry of Science of Colombia (Minciencias).
  • Pérez, Jorge A.: Support of the Dutch Research Council (NWO) under project No.016.Vidi.189.046 (Unifying Correctness for Communicating Software) is gratefully acknowledged.

Acknowledgements

We are most grateful to Bas van den Heuvel for initial discussions on the topic of this paper. We also thank the anonymous reviewers for their helpful suggestions.

Cite AsGet BibTex

Juan C. Jaramillo, Dan Frumin, and Jorge A. Pérez. Around Classical and Intuitionistic Linear Processes. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.30

Abstract

Curry-Howard correspondences between Linear Logic (LL) and session types provide a firm foundation for concurrent processes. As the correspondences hold for intuitionistic and classical versions of LL (ILL and CLL), we obtain two different families of type systems for concurrency. An open question remains: how do these two families exactly relate to each other? Based upon a translation from CLL to ILL due to Laurent, we provide two complementary answers, in the form of full abstraction results based on a typed observational equivalence due to Atkey. Our results elucidate hitherto missing formal links between seemingly related yet different type systems for concurrency.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Type theory
  • Theory of computation → Process calculi
Keywords
  • Process calculi
  • session types
  • linear logic

Metrics

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

Related Versions

References

  1. Robert Atkey. Observed communication semantics for classical processes. In Hongseok Yang, editor, Programming Languages and Systems, pages 56-82, Berlin, Heidelberg, 2017. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-54434-1_3.
  2. Robert Atkey, Sam Lindley, and J. Garrett Morris. Conflation Confers Concurrency, pages 32-55. Springer International Publishing, Cham, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_2.
  3. Stephanie Balzer and Frank Pfenning. Manifest sharing with session types. Proc. ACM Program. Lang., 1(ICFP):37:1-37:29, 2017. URL: https://doi.org/10.1145/3110281.
  4. Andrew Barber. Dual intuitionistic linear logic, 1996. Technical report, available at URL: https://www.lfcs.inf.ed.ac.uk/reports/96/ECS-LFCS-96-347/.
  5. Michele Boreale. On the expressiveness of internal mobility in name-passing calculi. Theoretical Computer Science, 195(2):205-226, 1998. Concurrency Theory. URL: https://doi.org/10.1016/S0304-3975(97)00220-X.
  6. Luís Caires and Jorge A. Pérez. Linearity, control effects, and behavioral types. 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 229-259. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_9.
  7. Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho. Domain-aware session types. In Wan J. Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands, volume 140 of LIPIcs, pages 39:1-39:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPICS.CONCUR.2019.39.
  8. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. 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 222-236. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_16.
  9. Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Math. Struct. Comput. Sci., 26(3):367-423, 2016. URL: https://doi.org/10.1017/S0960129514000218.
  10. Luís Caires and Bernardo Toninho. The session abstract machine. In Stephanie Weirich, editor, Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14576 of Lecture Notes in Computer Science, pages 206-235. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57262-3_9.
  11. Bor-Yuh Evan Chang, Kaustuv Chaudhuri, and Frank Pfenning. A judgmental analysis of linear logic. Technical Report CMU-CS-03-131R, Department of Computer Science, Carnegie Mellon University, November 2003. URL: https://doi.org/10.1184/R1/6587498.v1.
  12. Ornela Dardha and Simon J. Gay. A new linear logic for deadlock-free 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 91-109. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_5.
  13. Farzaneh Derakhshan, Stephanie Balzer, and Limin Jia. Session logical relations for noninterference. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470654.
  14. Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. Separating sessions smoothly. In Serge Haddad and Daniele Varacca, editors, 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 36:1-36:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.CONCUR.2021.36.
  15. Wen Kokke, Fabrizio Montesi, and Marco Peressotti. Better late than never: a fully-abstract semantics for classical processes. Proc. ACM Program. Lang., 3(POPL):24:1-24:29, 2019. URL: https://doi.org/10.1145/3290337.
  16. Olivier Laurent. Around classical and intuitionistic linear logics. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 629-638, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3209108.3209132.
  17. Frank Pfenning and Dennis Griffith. Polarized substructural session types. In Andrew M. Pitts, editor, Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9034 of Lecture Notes in Computer Science, pages 3-22. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46678-0_1.
  18. Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. Information and Computation, 239:254-302, 2014. URL: https://doi.org/10.1016/j.ic.2014.08.001.
  19. Zesen Qian, G. A. Kavvos, and Lars Birkedal. Client-server sessions in linear logic. Proc. ACM Program. Lang., 5(ICFP):1-31, 2021. URL: https://doi.org/10.1145/3473567.
  20. Harold Schellinx. Some Syntactical Observations on Linear Logic. Journal of Logic and Computation, 1(4):537-559, September 1991. URL: https://doi.org/10.1093/logcom/1.4.537.
  21. 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.
  22. Bas van den Heuvel and Jorge A. Pérez. Session type systems based on linear logic: Classical versus intuitionistic. In Stephanie Balzer and Luca Padovani, editors, Proceedings of the 12th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES@ETAPS 2020, Dublin, Ireland, 26th April 2020, volume 314 of EPTCS, pages 1-11, 2020. URL: https://doi.org/10.4204/EPTCS.314.1.
  23. Bas van den Heuvel and Jorge A. Pérez. Comparing session type systems derived from linear logic. CoRR, abs/2401.14763, 2024. URL: https://doi.org/10.48550/arXiv.2401.14763.
  24. Philip Wadler. Propositions as sessions. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP '12, pages 273-286, New York, NY, USA, 2012. Association for Computing Machinery. URL: https://doi.org/10.1145/2364527.2364568.
  25. Philip Wadler. Propositions as sessions. J. Funct. Program., 24(2-3):384-418, 2014. URL: https://doi.org/10.1017/S095679681400001X.
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