Brack: A Verified Compiler for Scheme via CakeML

Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs 2026 Open access

Read full text
Authors: Pascal Y. Lasnier, Jeremy Yallop, Magnus O. Myreen
DOI: 10.1145/3779031.3779098
Cited by: 1
References: 27

Abstract

This paper describes Brack, which is a new verified compiler for Scheme. Brack compiles a substantial subset of Scheme, including first-class continuations, recursive bindings, first-class functions, mutable local variables, and lists, to CakeML, from where programs can be compiled to machine code. Compilation from Scheme to CakeML is based around a continuation-passing-style (CPS) transformation that naturally arises from Scheme’s small-step semantics. We have formally established the correctness of Brack in the HOL4 theorem prover.

Fields of Study & Subjects

Logic programming and type systems Formal Methods in Verification Advanced Software Engineering Methodologies

Publication details

Journal / source
Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs
Publisher
ACM
Pages
157–170
Publication date
8 January 2026
Language
EN