Brack: A Verified Compiler for Scheme via CakeML

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.