Repository logo
 

Cakes That Bake Cakes: Dynamic Computation in CakeML

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Abstract

jats:pWe have extended the verified CakeML compiler with a new language primitive,
Eval, which permits evaluation of new CakeML syntax at runtime. This new
implementation supports an ambitious form of compilation at runtime and dynamic
execution, where the original and dynamically added code can share
(higher-order) values and recursively call each other. This is, to our
knowledge, the first verified run-time environment capable of supporting a
standard LCF-style theorem prover design.</jats:p> jats:pModifying the modern CakeML compiler pipeline and proofs to support
a dynamic computation semantics was an extensive project. We review the
design decisions, proof techniques, and proof engineering lessons
from the project, and highlight some unexpected complications.</jats:p>

Description

Keywords

compiler verification, dynamic computation, interactive theorem proving

Journal Title

Proceedings of the ACM on Programming Languages

Conference Name

PLDI 2023

Journal ISSN

2475-1421
2475-1421

Volume Title

Publisher

Association for Computing Machinery (ACM)
Sponsorship
European Research Council (789108)
Relationships
Is supplemented by: