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.2021.1
URN: urn:nbn:de:0030-drops-138963
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13896/
Go to the corresponding LIPIcs Volume Portal

Myreen, Magnus O.

The CakeML Project’s Quest for Ever Stronger Correctness Theorems (Invited Paper)

pdf-format:
LIPIcs-ITP-2021-1.pdf (0.5 MB)

Abstract

The CakeML project has developed a proof-producing code generation mechanism for the HOL4 theorem prover, a verified compiler for ML and, using these, a number of verified application programs that are proved correct down to the machine code that runs them (in some cases, even down to the underlying hardware). The purpose of this extended abstract is to tell the story of the project and to point curious readers to publications where they can read more about specific contributions.

BibTeX - Entry

@InProceedings{myreen:LIPIcs.ITP.2021.1,
  author =	{Myreen, Magnus O.},
  title =	{{The CakeML Project’s Quest for Ever Stronger Correctness Theorems}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{1:1--1:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13896},
  URN =		{urn:nbn:de:0030-drops-138963},
  doi =		{10.4230/LIPIcs.ITP.2021.1},
  annote =	{Keywords: Program verification, interactive theorem proving}
}

Keywords: Program verification, interactive theorem proving
Collection: 12th International Conference on Interactive Theorem Proving (ITP 2021)
Issue Date: 2021
Date of publication: 21.06.2021
Supplementary Material: https://cakeml.org

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