Certified Compilation of Choreographies with hacc

Luís Cruz-Filipe, Lovro Lugovic, Fabrizio Montesi [2023].
In proceedings of FORTE 2023, pp. 29-36.

Abstract

Programming communicating processes is challenging, because it requires writing separate programs that perform compatible send and receive actions at the right time during execution. Leaving this task to the programmer can easily lead to bugs. Choreographic programming addresses this challenge by equipping developers with high-level abstractions for codifying the desired communication structures from a global viewpoint. Given a choreography, implementations of the involved processes can be automatically generated by endpoint projection (EPP).

While choreographic programming prevents manual mistakes in the implementation of communications, the correctness of a choreographic programming framework crucially hinges on the correctness of its complex compiler, which has motivated formalisation of theories of choreographic programming in theorem provers. In this paper, we build upon one of these formalisations to construct a toolchain that produces executable code from a choreography.

Links

doi.org

Additional notes

None

Cite (BibTeX)

Click to expand

@inproceedings{DBLP:conf/forte/Cruz-FilipeLM23,
  author       = {Lu{\'{\i}}s Cruz{-}Filipe and
                  Lovro Lugovic and
                  Fabrizio Montesi},
  editor       = {Marieke Huisman and
                  Ant{\'{o}}nio Ravara},
  title        = {Certified Compilation of Choreographies with hacc},
  booktitle    = {Formal Techniques for Distributed Objects, Components, and Systems
                  - 43rd {IFIP} {WG} 6.1 International Conference, {FORTE} 2023, Held
                  as Part of the 18th International Federated Conference on Distributed
                  Computing Techniques, DisCoTec 2023, Lisbon, Portugal, June 19-23,
                  2023, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {13910},
  pages        = {29--36},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-35355-0\_3},
  doi          = {10.1007/978-3-031-35355-0\_3},
  timestamp    = {Fri, 07 Jul 2023 23:30:53 +0200},
  biburl       = {https://dblp.org/rec/conf/forte/Cruz-FilipeLM23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

A PDF is available (possibly a preprint):

Some data from DBLP and Crossref.