An Overview of the CakeML verified compiler and some new challenges

Add to your list(s) Download to your calendar using vCal

• Thomas Sewell
• Friday 06 March 2020, 10:00-10:20
• Computer Lab, FW26.

If you have a question about this talk, please contact Jean Pichon-Pharabod.

This talk has been canceled/deleted

The CakeML project has developed a self-hosting verified compiler for a language in the ML family. I’ve joined the project recently, and have been working on dynamic code execution. I’ll give an overview of the compiler design and proof design, and discuss why dynamic code (Eval) introduces some new and old challenges.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

This talk is not included in any other list

Note that ex-directory lists are not shown.