Principles of Programming Seminar
Speaker
OSKAR ABRAHAMSSON, MAGNUS O. MYREEN
Oskar: Ph.D. Student
Magnus: Associate Professor
Chalmers University of Technology
When
-
Where
In Person and Zoom
Description
The CakeML project has explored many aspects of programming languages in a setting of formal proofs. Topics include: semantics, type systems, verified compilation, proof-producing code generation, program logics, compiler bootstrapping and more. This talk will present a major case study that builds on almost every part of the CakeML project, more specifically, our work on the verified Candle theorem prover.
The Candle theorem prover is our verified clone of the HOL light theorem prover. Our verification proof of this new theorem prover implementation results in an end-to-end correctness theorem that guarantees the soundness of the entire system down to the machine code that executes at runtime. Our end-to-end theorem states that every exported fact produced by this machine-code program is valid in higher-order logic. Candle consists of a proved-to-be-safe interactive read-eval-print loop (REPL) that executes the CakeML compiler internally for the “eval” part of “read-eval-print loop”. Throughout this work, we have strived to make the Candle’s REPL provide a user experience as close to HOL Light’s as possible. To this end, we have made it parse HOL light’s version of OCaml syntax.
The Candle prover is available for download.
Additional Reading
The CakeML project lives in the HOL4 theorem prover
—
• Oskar Abrahamsson is a PhD student at Chalmers University of Technology since 2017, supervised by Assoc. Prof. Magnus Myreen. Abrahamsson has a BSc in Applied Mathematics (2012-2015), and an MSc in Computer Science (2015-2017) from Chalmers, Sweden.
• Magnus Myreen did his PhD in Cambridge UK during 2005-2008, supervised by Prof. Mike Gordon. After his PhD, Myreen stayed on at Cambridge, first as a postdoc on his own grant and then as a Royal Society University Fellow. In 2014, Myreen moved to Chalmers University of Technology, where he became a tenured Associate Professor in 2015.
In Person and Zoom Participation. See announcement.