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

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

• Magnus Myreen ( Chalmers University, Sweden)
• Friday 21 June 2024, 14:00-15:00
• TBC - probably SS03, Computer Laboratory.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• TBC - probably SS03, Computer Laboratory
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.