Document Open Access Logo

Formalising a Turing-Complete Choreographic Language in Coq

Authors Luís Cruz-Filipe , Fabrizio Montesi , Marco Peressotti

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.15.pdf
  • Filesize: 0.63 MB
  • 18 pages

Document Identifiers

Author Details

Luís Cruz-Filipe
  • Department Mathematics and Computer Science, University of Southern Denmark, Odense, Denmark
Fabrizio Montesi
  • Department Mathematics and Computer Science, University of Southern Denmark, Odense, Denmark
Marco Peressotti
  • Department Mathematics and Computer Science, University of Southern Denmark, Odense, Denmark

Funding

Work partially supported by Villum Fonden, grant no. 29518.

Cite AsGet BibTex

Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. Formalising a Turing-Complete Choreographic Language in Coq. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ITP.2021.15

Abstract

The theory of choreographic languages typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of them lead to long reviewing processes, and occasionally to errors being found in published proofs. In this work, we take a published proof of Turing completeness of a choreographic language and formalise it in Coq. Our development includes formalising the choreographic language, its basic properties, Kleene’s theory of partial recursive functions, the encoding of these functions as choreographies, and a proof that this encoding is correct. With this effort, we show that theorem proving can be a very useful tool in the field of choreographic languages: besides the added degree of confidence that we get from a mechanised proof, the formalisation process led us to a significant simplification of the underlying theory. Our results offer a foundation for the future formal development of choreographic languages.

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
  • Theory of computation → Recursive functions
  • Theory of computation → Logic and verification
Keywords
  • Choreographic Programming
  • Formalisation
  • Turing Completeness

Metrics

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

Related Versions

Supplementary Materials

References

  1. 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. Foundations and Trends in Programming Languages, 3(2-3):95-230, 2016. Google Scholar
  2. Samik Basu, Tevfik Bultan, and Meriem Ouederni. Deciding choreography realizability. In John Field and Michael Hicks, editors, Procs. POPL, pages 191-202. ACM, 2012. URL: https://doi.org/10.1145/2103656.2103680.
  3. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In Paul Gastin and François Laroussinie, editors, Procs. CONCUR, 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.
  4. Marco Carbone, Kohei Honda, and Nobuko Yoshida. Structured communication-centered programming for web services. ACM Trans. Program. Lang. Syst., 34(2):8:1-8:78, 2012. URL: https://doi.org/10.1145/2220365.2220367.
  5. Marco Carbone and Fabrizio Montesi. Deadlock-freedom-by-design: multiparty asynchronous global programming. In Roberto Giacobazzi and Radhia Cousot, editors, Procs. POPL, pages 263-274. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429101.
  6. Luís Cruz-Filipe and Fabrizio Montesi. Choreographies in practice. In Elvira Albert and Ivan Lanese, editors, Procs. FORTE, volume 9688 of Lecture Notes in Computer Science, pages 114-123. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-39570-8_8.
  7. Luís Cruz-Filipe and Fabrizio Montesi. A core model for choreographic programming. Theor. Comput. Sci., 802:38-66, 2020. URL: https://doi.org/10.1016/j.tcs.2019.07.005.
  8. Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. Choreographies in Coq. In TYPES 2019, Abstracts, 2019. Extended abstract. Google Scholar
  9. Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. Certifying choreography compilation. CoRR, abs/2102.10698, 2021. URL: https://arxiv.org/abs/2102.10698.
  10. Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. A formalisation of a Turing-complete choreographic language in Coq, 2021. URL: https://doi.org/10.5281/zenodo.4479102.
  11. Mila Dalla Preda, Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, and Jacopo Mauro. Dynamic choreographies: Theory and implementation. Log. Methods Comput. Sci., 13(2), 2017. URL: https://doi.org/10.23638/LMCS-13(2:1)2017.
  12. Yannick Forster, Dominik Kirst, and Gert Smolka. On synthetic undecidability in Coq, with an application to the Entscheidungsproblem. In Assia Mahboubi and Magnus O. Myreen, editors, Procs. CPP, pages 38-51. ACM, 2019. URL: https://doi.org/10.1145/3293880.3294091.
  13. Yannick Forster, Fabian Kunze, and Maximilian Wuttke. Verified programming of Turing machines in Coq. In Jasmin Blanchette and Cătălin Hricommabelowtcu, editors, Procs. CPP, pages 114-128. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373816.
  14. Simon J. Gay, Vasco T. Vasconcelos, Philip Wadler, and Nobuko Yoshida. Theory and applications of behavioural types (Dagstuhl Seminar 17051). Dagstuhl Reports, 7(1):158-189, 2017. URL: https://doi.org/10.4230/DagRep.7.1.158.
  15. Saverio Giallorenzo, Ivan Lanese, and Daniel Russo. Chip: A choreographic integration process. In Hervé Panetto, Christophe Debruyne, Henderik A. Proper, Claudio Agostino Ardagna, Dumitru Roman, and Robert Meersman, editors, Procs. OTM, part II, volume 11230 of Lecture Notes in Computer Science, pages 22-40. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02671-4_2.
  16. Saverio Giallorenzo, Fabrizio Montesi, and Marco Peressotti. Choreographies as objects. CoRR, abs/2005.09520, 2020. URL: https://arxiv.org/abs/2005.09520.
  17. Alejandro Gomez-Londono and Johannes Aman Pohjola. Connecting choreography languages with verified stacks. In Procs. of the Nordic Workshop on Programming Theory, pages 31-33, 2018. URL: http://hdl.handle.net/102.100.100/86327?index=1.
  18. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9, 2016. Also: POPL, pages 273-284, 2008. URL: https://doi.org/10.1145/2827695.
  19. 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.
  20. Intl. Telecommunication Union. Recommendation Z.120: Message Sequence Chart, 1996. Google Scholar
  21. Stephen Cole Kleene. Introduction to Metamathematics, volume 1. North-Holland Publishing Co., 1952. Google Scholar
  22. Alberto Lluch-Lafuente, Flemming Nielson, and Hanne Riis Nielson. Discretionary information flow control for interaction-oriented specifications. In Narciso Martí-Oliet, Peter Csaba Ölveczky, and Carolyn L. Talcott, editors, Logic, Rewriting, and Concurrency, volume 9200 of Lecture Notes in Computer Science, pages 427-450. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23165-5_20.
  23. Alejandro Gómez Londoño. Choreographies and cost semantics for reliable communicating systems. Licentiate thesis, Chalmers University of Technology, 2020. Google Scholar
  24. Hugo A. López and Kai Heussen. Choreographing cyber-physical distributed control systems for the energy sector. In Ahmed Seffah, Birgit Penzenstadler, Carina Alves, and Xin Peng, editors, Procs. SAC, pages 437-443. ACM, 2017. URL: https://doi.org/10.1145/3019612.3019656.
  25. Hugo A. López, Flemming Nielson, and Hanne Riis Nielson. Enforcing availability in failure-aware communicating systems. In Elvira Albert and Ivan Lanese, editors, Procs. FORTE, volume 9688 of Lecture Notes in Computer Science, pages 195-211. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-39570-8_13.
  26. Petar Maksimovic and Alan Schmitt. HOCore in Coq. In Christian Urban and Xingyuan Zhang, editors, Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings, volume 9236 of Lecture Notes in Computer Science, pages 278-293. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-22102-1_19.
  27. Fabrizio Montesi. Choreographic Programming. Ph.D. Thesis, IT University of Copenhagen, 2013. URL: http://www.fabriziomontesi.com/files/choreographic_programming.pdf.
  28. Fabrizio Montesi. Introduction to Choreographies. Accepted for publication by Cambridge University Press, 2020. Google Scholar
  29. Roger M. Needham and Michael D. Schroeder. Using encryption for authentication in large networks of computers. Commun. ACM, 21(12):993-999, 1978. URL: https://doi.org/10.1145/359657.359659.
  30. Object Management Group. Business Process Model and Notation. http://www.omg.org/spec/BPMN/2.0/, 2011.
  31. 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.
  32. Alan M. Turing. Computability and λ-definability. J. Symb. Log., 2(4):153-163, 1937. URL: https://doi.org/10.2307/2268280.
  33. W3C. WS Choreography Description Language. http://www.w3.org/TR/ws-cdl-10/, 2004.
  34. Vincent Zammit. A proof of the s-m-n theorem in coq. Technical report, The Computing Laboratory, The University of Kent, Canterbury, Kent, UK, 1997. URL: https://kar.kent.ac.uk/21524/.
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