Certified compilation of choreographies with \textsf{hacc}

DOI10.1007/978-3-031-35355-0_3MaRDI QIDQ6535459zbMATH OpenFDO

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

Publication date 11 January 2024

Full work available at URL https://doi.org/10.1007/978-3-031-35355-0_3

zbMATH Keywords

certified compilationchoreographic programmingformal verificationJolie

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Applied Choreographies
• Choreographies, logically
• Choreographies, logically
• A core model for choreographic programming

Cites work

• A core model for choreographic programming
• A formal theory of choreographic programming
• Certifying choreography compilation
• Deadlock-freedom-by-design, multiparty asynchronous global programming
• scientific article; zbMATH DE number 7699432 (Why is no real title available?)
• Kalas: a verified, end-to-end compiler for a choreographic language
• Procedural Choreographic Programming
• Proof-producing synthesis of ML from higher-order logic

Cited in

(1)

• An abstract framework for choreographic testing

This page was built for publication: Certified compilation of choreographies with \textsf{hacc}

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535459)