Document Open Access Logo

A Sound and Complete Projection for Global Types

Authors Dawit Tirore, Jesper Bengtson, Marco Carbone

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2023.28.pdf
  • Filesize: 0.88 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Computing methodologies → Distributed programming languages
  • Theory of computation → Program verification
Keywords
  • Session types
  • Mechanisation
  • Projection
  • Coq

Metrics

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

Abstract

Multiparty session types is a typing discipline used to write specifications, known as global types, for branching and recursive message-passing systems. A necessary operation on global types is projection to abstractions of local behaviour, called local types. Typically, this is a computable partial function that given a global type and a role erases all details irrelevant to this role.
Computable projection functions in the literature are either unsound or too restrictive when dealing with recursion and branching. Recent work has taken a more general approach to projection defining it as a coinductive, but not computable, relation. Our work defines a new computable projection function that is sound and complete with respect to its coinductive counterpart and, hence, equally expressive. All results have been mechanised in the Coq proof assistant.

Cite As Get BibTex

Dawit Tirore, Jesper Bengtson, and Marco Carbone. A Sound and Complete Projection for Global Types. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.ITP.2023.28

Author Details

Dawit Tirore
  • IT University of Copenhagen, Denmark
Jesper Bengtson
  • IT University of Copenhagen, Denmark
Marco Carbone
  • IT University of Copenhagen, Denmark

Funding

This work was supported by DFF-Research Project 1 Grant no. 1026-00385A, from The Danish Council for Independent Research for the Natural Sciences (FNU).

Supplementary Materials

References

  1. Coinductive types and corecursive functions. https://coq.inria.fr/refman/language/core/coinductive.html. Accessed: May 2023.
  2. Session types in programming languages: A collection of implementations. http://www.simonjf.com/2016/05/28/session-type-implementations.html. Accessed: May 2023.
  3. Andrea Asperti. A compact proof of decidability for regular expression equivalence. In proceedings of ITP, volume 7406 of LNCS, pages 283-298. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32347-8_19.
  4. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. The Matita interactive theorem prover. In Proceedings of CADE, volume 6803 of LNCS, pages 64-69. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22438-6_7.
  5. Andi Bejleri and Nobuko Yoshida. Synchronous multiparty session types. In Proceedings of PLACES, volume 241 of ENTCS, pages 3-33. Elsevier, 2008. URL: https://doi.org/10.1016/j.entcs.2009.06.002.
  6. Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. URL: https://doi.org/10.1007/978-3-662-07964-5.
  7. David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, and Nobuko Yoshida. Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes. In Proceedings of PLDI, pages 237-251. ACM, 2021. URL: https://doi.org/10.1145/3453483.3454041.
  8. Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. Certifying choreography compilation. In Antonio Cerone and Peter Csaba Ölveczky, editors, Proceedings of ICTAC 2021, volume 12819 of Lecture Notes in Computer Science, pages 115-133. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-85315-0_8.
  9. Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. Formalising a turing-complete choreographic language in coq. In Liron Cohen and Cezary Kaliszyk, editors, Proceedings of ITP 2021, volume 193 of LIPIcs, pages 15:1-15:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.15.
  10. Nicolaas Govert de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381-392, 1972. URL: https://doi.org/10.1016/1385-7258(72)90034-0.
  11. Romain Demangeon and Nobuko Yoshida. On the expressiveness of multiparty sessions. In Proceedings of FSTTCS, volume 45 of LIPIcs, pages 560-574, 2015. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2015.560.
  12. Simon Gay and Vasco Vasconcelos. Linear type theory for asynchronous session types. Journal of Functional Programming, 20(1):19-50, 2010. URL: https://doi.org/10.1017/S0956796809990268.
  13. Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions. Journal of Logical and Albegraic Methods in Programming, 104:127-173, 2019. URL: https://doi.org/10.1016/j.jlamp.2018.12.002.
  14. Georges Gonthier, Assia Mahboubi, and Enrico Tassi. A small scale reflection extension for the coq system, 2016. URL: https://inria.hal.science/inria-00258384.
  15. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Proceedings of ESOP, volume 1381 of LNCS, pages 122-138. Springer, 1998. URL: https://doi.org/10.1007/BFb0053567.
  16. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Proceedings of POPL, pages 273-284. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328472.
  17. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. Journal of the ACM, 63(1):9:1-9:67, 2016. URL: https://doi.org/10.1145/2827695.
  18. Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. The power of parameterization in coinductive proof. In Proceedings of POPL, pages 193-206. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429093.
  19. Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. Multiparty GV: functional multiparty session types with certified deadlock freedom. Proceedings of the ACM on Programming Languages, 6(ICFP):466-495, 2022. URL: https://doi.org/10.1145/3547638.
  20. Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. Cocaml: Functional programming with regular coinductive types. Fundamenta Informaticae, 150:347-377, 2017. URL: https://doi.org/10.3233/FI-2017-1473.
  21. The Coq development team. The Coq Proof Assistant. https://coq.inria.fr. Accessed: May 2023.
  22. Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. Google Scholar
  23. Alceste Scalas and Nobuko Yoshida. Less is more: multiparty session types revisited. Proc. ACM Program. Lang., 3(POPL):30:1-30:29, 2019. URL: https://doi.org/10.1145/3290343.
  24. Matthieu Sozeau and Cyprien Mangin. Equations reloaded: High-level dependently-typed functional programming and proving in coq. Proceedings of the ACM on Programming Languages, 3(ICFP):86:1-86:29, 2019. URL: https://doi.org/10.1145/3341690.
  25. Kathrin Stark, Steven Schäfer, and Jonas Kaiser. Autosubst 2: reasoning with multi-sorted de bruijn terms and vector substitutions. In Proceedings of CPP, pages 166-180. ACM, 2019. URL: https://doi.org/10.1145/3293880.3294101.
  26. Huub ten Eikelder. Some algorithms to decide the equivalence of recursive types. https://pure.tue.nl/ws/files/2150345/9211264.pdf, 1991. Accessed: May 2023.
  27. Rob van Glabbeek, Peter Höfner, and Ross Horne. Assuming just enough fairness to make session types complete for lock-freedom. In Proceedings of LICS, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470531.
  28. Philip Wadler. Propositions as sessions. In Proceedings of ICFP, pages 273-286. ACM, 2012. URL: https://doi.org/10.1145/2364527.2364568.
  29. Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic. An equational theory for weak bisimulation via generalized parameterized coinduction. In Proceedings of CPP, pages 71-84. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373813.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact