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

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

An Overview of the CakeML verified compiler and some new challenges

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.

This talk is included in these lists:

  • This talk is not included in any other list

Note that ex-directory lists are not shown.

Other lists

Lecture Theatre, MRC Cognition and Brain Sciences Unit, Chaucer Road Cavendish Laboratory, Pippard Lecture Theatre & TEAMS Zoom (copy link or see details below) bit.ly/2PMNjMS

Other talks

Feedback and the circumgalactic medium Emergency Medicine and Metabolic Medicine Group Presentation 2 Morning Break Group Work TBC
 

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