BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Much Still to Do in Compiler Verification (A Perspective from the 
 CakeML Project) - Magnus Myreen ( Chalmers University\, Sweden)
DTSTART:20240621T130000Z
DTEND:20240621T140000Z
UID:TALK218095@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:Compiler verification is an area that has grown considerably i
 n the\nlast 20 years and a newcomer or outsider might mistakenly think tha
 t\nthe area is quite crowded. In this talk\, I will argue that the state\n
 of the art in compiler verification is still quite far from where it\nough
 t to be -- there is still plenty to do!\n\nThis talk will be given from th
 e perspective of the CakeML project\,\nwhich has developed an end-to-end v
 erified compiler for an ML-like\nprogramming language and is perhaps best 
 known as the first formally\nverified compiler to be bootstrapped inside t
 he logic of a proof\nassistant.\n\nThe focus will be on the research quest
 ions: both questions the CakeML\nproject has tackled and yet-to-be-satisfa
 ctorily addressed questions\nthat have emerged when attempting to make ver
 ified compilers as\nrealistic and far reaching as possible. The questions 
 will revolve\naround work on top of verified memory management and ruling 
 out\nunwanted out-of-memory errors\, using verified compilers in verified\
 napplications and verified stacks\, making (components of) verified\ncompi
 lers more reusable\, exploring paths to wider use of verified\ncompilers\,
  etc.\n\nMy intention is to provide ideas where the current state of the a
 rt in\ncompiler verification leaves room for exciting new work.
LOCATION:TBC - probably SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR