2026-07-22T04:54:16Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16736 2024-03-06T10:58:11Z ddc:004 open_access

Kalas: A Verified, End-To-End Compiler for a Choreographic Language Pohjola, Johannes Åman Gómez-Londoño, Alejandro Shaker, James Norrish, Michael Choreographies Interactive Theorem Proving Compiler Verification Choreographies are an abstraction for globally describing deadlock-free communicating systems. A choreography can be compiled into multiple endpoints preserving the global behavior, providing a path for concrete system implementations. Of course, the soundness of this approach hinges on the correctness of the compilation function. In this paper, we present a verified compiler for Kalas, a choreographic language. Its machine-checked end-to-end proof of correctness ensures all generated endpoints adhere to the system description, preserving the top-level communication guarantees. This work uses the verified CakeML compiler and Hol4 proof assistant, allowing for concrete executable implementations and statements of correctness at the machine code level for multiple architectures. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Johannes Åman Pohjola and Alejandro Gómez-Londoño and James Shaker and Michael Norrish 2022 Is Part Of LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2022.27 urn:nbn:de:0030-drops-167368 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.27 eng https://creativecommons.org/licenses/by/4.0/legalcode