University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > An Overview of the CakeML verified compiler and some new challenges

An Overview of the CakeML verified compiler and some new challenges

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

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.

Tell a friend about this talk:

This talk is included in these lists:

This talk is not included in any other list

Note that ex-directory lists are not shown.

 

© 2006-2021 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity