POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Mon 12 Jan 2026 16:22 - 16:45 at Belvédère - Compilers Chair(s): Matthieu Sozeau

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 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

16:00 - 17:30
CompilersCPP at Belvédère
Chair(s): Matthieu Sozeau Inria
16:00
22m
Talk
Mechanized Dominator Tree Certificationdistinguished paper
CPP
Jean-Christophe Léchenet Université Côte d’Azur, Inria
DOI Pre-print
16:22
22m
Talk
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
22m
Talk
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
22m
Talk
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