University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Much Still to Do in Compiler Verification (A Perspective from the CakeML Project)

Much Still to Do in Compiler Verification (A Perspective from the CakeML Project)

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

If you have a question about this talk, please contact Peter Sewell.

Compiler verification is an area that has grown considerably in the last 20 years and a newcomer or outsider might mistakenly think that the area is quite crowded. In this talk, I will argue that the state of the art in compiler verification is still quite far from where it ought to be—there is still plenty to do!

This talk will be given from the perspective of the CakeML project, which has developed an end-to-end verified compiler for an ML-like programming language and is perhaps best known as the first formally verified compiler to be bootstrapped inside the logic of a proof assistant.

The focus will be on the research questions: both questions the CakeML project has tackled and yet-to-be-satisfactorily addressed questions that have emerged when attempting to make verified compilers as realistic and far reaching as possible. The questions will revolve around work on top of verified memory management and ruling out unwanted out-of-memory errors, using verified compilers in verified applications and verified stacks, making (components of) verified compilers more reusable, exploring paths to wider use of verified compilers, etc.

My intention is to provide ideas where the current state of the art in compiler verification leaves room for exciting new work.

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:

Note that ex-directory lists are not shown.


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