Certified Compilation of Choreographies with hacc

Luís Cruz-Filipe, Lovro Lugović*, Fabrizio Montesi

*Kontaktforfatter

Publikation: Kapitel i bog/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

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.

OriginalsprogEngelsk
TitelFormal Techniques for Distributed Objects, Components, and Systems
RedaktørerMarieke Huisman, António Ravara
ForlagSpringer Science+Business Media
Publikationsdato2023
Sider29-36
ISBN (Trykt)9783031353543
DOI
StatusUdgivet - 2023
Begivenhed43rd IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2023, held as part of the 18th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023 - Lisbon, Portugal
Varighed: 19. jun. 202323. jun. 2023

Konference

Konference43rd IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2023, held as part of the 18th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023
Land/OmrådePortugal
ByLisbon
Periode19/06/202323/06/2023
NavnLecture Notes in Computer Science
Vol/bind13910 LNCS
ISSN0302-9743

Bibliografisk note

Funding Information:
This work was partially supported by Villum Fonden, grant no. 29518, and the Independent Research Fund Denmark, grant no. 0135-00219.

Publisher Copyright:
© 2023, IFIP International Federation for Information Processing.

Fingeraftryk

Dyk ned i forskningsemnerne om 'Certified Compilation of Choreographies with hacc'. Sammen danner de et unikt fingeraftryk.

Citationsformater