1 Search Results for "Shaker, James"

Document
DOI: 10.4230/LIPIcs.ITP.2022.27
Kalas: A Verified, End-To-End Compiler for a Choreographic Language

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

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

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.
Cite as

Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, and Michael Norrish. Kalas: A Verified, End-To-End Compiler for a Choreographic Language. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.27},
  URN =		{urn:nbn:de:0030-drops-167368},
  doi =		{10.4230/LIPIcs.ITP.2022.27},
  annote =	{Keywords: Choreographies, Interactive Theorem Proving, Compiler Verification}
}
  • Refine by Author
  • 1 Gómez-Londoño, Alejandro
  • 1 Norrish, Michael
  • 1 Pohjola, Johannes Åman
  • 1 Shaker, James

  • Refine by Classification
  • 1 Software and its engineering → Compilers
  • 1 Software and its engineering → Software verification
  • 1 Theory of computation → Concurrency

  • Refine by Keyword
  • 1 Choreographies
  • 1 Compiler Verification
  • 1 Interactive Theorem Proving

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact