BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:The CakeML Project: Verified Compilation\, Verified Bootstrapping\
 , Just-In-Time Compilation\, and Applications
DTSTART:20230314T100000
DTEND:20230314T110000
DTSTAMP:20260407T060536Z
UID:fa3b95aaf1b8716084651885907e460f6073984c1673d51b1b663dc1
CATEGORIES:Conferences - Seminars
DESCRIPTION:Magnus Myreen (Chalmers University of Technology)\nThis talk w
 ill be about the CakeML project. The CakeML project centres around an impu
 re functional programming language\, for which we have developed a collect
 ion of proofs and tools inside the HOL4 theorem prover. The development in
 cludes a proven-correct compiler that can bootstrap itself.\n\nThis talk h
 as two parts.\n\nIn the first part\, I will explain the research questions
  the CakeML project has tackled and outline the main research ideas that h
 ave helped us address them. The research questions include:\n\n	how can we
  transfer properties proved of logic functions to properties of machine co
 de compiled from those functions?\n	how can we use a verified compiler to 
 compile itself?\n	how can we reason about space usage of CakeML programs?\
 n	how can we prove liveness properties for non-terminating code?\n\nIn the
  second part\, I will describe how the CakeML project strives to build mea
 ningful connections with other projects and our experience with this so fa
 r. We have:\n\n\n	built a proved-to-be-sound clone of the HOL light theore
 m prover\n	produced a verified compiler for a Haskell-like language\n	cons
 tructed several verified checkers\, including checkers for UNSAT proofs\, 
 floating-point error bounds\, OpenTheory article files\, pseudo- Boolean p
 roofs\, and Integer Programming proofs\n\nThe CakeML project is an open pr
 oject and we are always keen to explore new collaborations.\nThe CakeML we
 bpage: https://cakeml.org/\nThe CakeML project lives in the HOL4 theorem 
 prover: https://hol-theorem-prover.org/\n 
LOCATION:INM 11 https://plan.epfl.ch/?room==INM%2011
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR