Certified Compilation of Choreographies with hacc

Luís Cruz-Filipe; Lovro Lugović; Fabrizio Montesi

doi:10.1007/978-3-031-35355-0_3

Certified Compilation of Choreographies with hacc

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

^*Corresponding author for this work

University of Southern Denmark

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-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.

Original language	English
Title of host publication	Formal Techniques for Distributed Objects, Components, and Systems
Editors	Marieke Huisman, António Ravara
Publisher	Springer Science+Business Media
Publication date	2023
Pages	29-36
ISBN (Print)	9783031353543
DOIs	https://doi.org/10.1007/978-3-031-35355-0_3
Publication status	Published - 2023
Event	43rd 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 Duration: 19. Jun 2023 → 23. Jun 2023

Conference

Conference	43rd 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
Country/Territory	Portugal
City	Lisbon
Period	19/06/2023 → 23/06/2023

Series	Lecture Notes in Computer Science
Volume	13910 LNCS
ISSN	0302-9743

Keywords

Certified compilation
Choreographic programming
Formal verification
Jolie

Documents & Links

10.1007/978-3-031-35355-0_3

https://arxiv.org/pdf/2303.03972.pdf

1 Ph.D. thesis

Choreographic Programming in the Mainstream
Lugović, L., 14. Mar 2024, Syddansk Universitet. Det Naturvidenskabelige Fakultet. 126 p.
Research output: Thesis › Ph.D. thesis

Cite this

@inproceedings{77bf66d38e09485d9aecb61ffbbc71d6,

title = "Certified Compilation of Choreographies with hacc",

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.",

keywords = "Certified compilation, Choreographic programming, Formal verification, Jolie",

author = "Lu{\'i}s Cruz-Filipe and Lovro Lugovi{\'c} and Fabrizio Montesi",

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: {\textcopyright} 2023, IFIP International Federation for Information Processing.; 43rd 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 ; Conference date: 19-06-2023 Through 23-06-2023",

year = "2023",

doi = "10.1007/978-3-031-35355-0_3",

language = "English",

isbn = "9783031353543",

series = "Lecture Notes in Computer Science",

publisher = "Springer Science+Business Media",

pages = "29--36",

editor = "Marieke Huisman and Ant{\'o}nio Ravara",

booktitle = "Formal Techniques for Distributed Objects, Components, and Systems",

address = "United States",

}

Cruz-Filipe, L, Lugović, L & Montesi, F 2023, Certified Compilation of Choreographies with hacc. in M Huisman & A Ravara (eds), Formal Techniques for Distributed Objects, Components, and Systems. Springer Science+Business Media, Lecture Notes in Computer Science, vol. 13910 LNCS, pp. 29-36, 43rd 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, 19/06/2023. https://doi.org/10.1007/978-3-031-35355-0_3

Certified Compilation of Choreographies with hacc. / Cruz-Filipe, Luís; Lugović, Lovro; Montesi, Fabrizio.
Formal Techniques for Distributed Objects, Components, and Systems. ed. / Marieke Huisman; António Ravara. Springer Science+Business Media, 2023. p. 29-36 (Lecture Notes in Computer Science, Vol. 13910 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Certified Compilation of Choreographies with hacc

AU - Cruz-Filipe, Luís

AU - Lugović, Lovro

AU - Montesi, Fabrizio

N1 - 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.

PY - 2023

Y1 - 2023

N2 - 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.

AB - 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.

KW - Certified compilation

KW - Choreographic programming

KW - Formal verification

KW - Jolie

U2 - 10.1007/978-3-031-35355-0_3

DO - 10.1007/978-3-031-35355-0_3

M3 - Article in proceedings

AN - SCOPUS:85164267408

SN - 9783031353543

T3 - Lecture Notes in Computer Science

SP - 29

EP - 36

BT - Formal Techniques for Distributed Objects, Components, and Systems

A2 - Huisman, Marieke

A2 - Ravara, António

PB - Springer Science+Business Media

T2 - 43rd 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

Y2 - 19 June 2023 through 23 June 2023

ER -

Certified Compilation of Choreographies with hacc

Abstract

Conference

Keywords

Documents & Links

Fingerprint

Related research output

Choreographic Programming in the Mainstream

Cite this