Certified compilation of choreographies with \textsf{hacc}

DOI10.1007/978-3-031-35355-0_3MaRDI QIDQ6535459zbMATHFDO

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

Publication date 11 January 2024

zbMATH Keywords

formal verificationchoreographic programmingcertified compilationJolie

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) 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

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

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)