License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.27
URN: urn:nbn:de:0030-drops-167368
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16736/
Go to the corresponding LIPIcs Volume Portal

Pohjola, Johannes Åman ; Gómez-Londoño, Alejandro ; Shaker, James ; Norrish, Michael

Kalas: A Verified, End-To-End Compiler for a Choreographic Language

pdf-format:
LIPIcs-ITP-2022-27.pdf (0.9 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{pohjola_et_al:LIPIcs.ITP.2022.27,
  author =	{Pohjola, Johannes \r{A}man and G\'{o}mez-Londo\~{n}o, Alejandro and Shaker, James and Norrish, Michael},
  title =	{{Kalas: A Verified, End-To-End Compiler for a Choreographic Language}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{27:1--27:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16736},
  URN =		{urn:nbn:de:0030-drops-167368},
  doi =		{10.4230/LIPIcs.ITP.2022.27},
  annote =	{Keywords: Choreographies, Interactive Theorem Proving, Compiler Verification}
}

Keywords: Choreographies, Interactive Theorem Proving, Compiler Verification
Collection: 13th International Conference on Interactive Theorem Proving (ITP 2022)
Issue Date: 2022
Date of publication: 03.08.2022
Supplementary Material: Software (Source Code): https://github.com/CakeML/choreo/

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI