POPL 2026 (series) / CPP 2026 (series) / CPP 2026 /
Brack: A Verified Compiler for Scheme via CakeML
This paper describes Brack, which is a new verified compiler for Scheme. Brack compiles a substantial subset of Scheme, which includes 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.
Mon 12 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Mon 12 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
16:00 - 17:30 | |||
16:00 22mTalk | Mechanized Dominator Tree Certificationdistinguished paper CPP Jean-Christophe Léchenet Université Côte d’Azur, Inria DOI Pre-print | ||
16:22 22mTalk | Brack: A Verified Compiler for Scheme via CakeML CPP Pascal Lasnier University of Cambridge, Jeremy Yallop University of Cambridge, Magnus O. Myreen Chalmers University of Technology | ||
16:45 22mTalk | Verified VCG and Verified Compiler for Dafny CPP Daniel Nezamabadi NTU Singapore, Magnus O. Myreen Chalmers University of Technology, Yong Kiam Tan Institute for Infocomm Research, A*STAR | ||
17:07 22mTalk | Foundational Verification of Running-Time Bounds for Interactive Programs CPP Thomas Carotti MIT, Andy Tockman Massachussetts Institute of Technology, Pratap Singh CMU, Andres Erbsen Google, Samuel Gruetter ETH Zurich, Adam Chlipala Massachusetts Institute of Technology | ||