LFCS seminar : Magnus Myreen: CakeML: a formally verified implementation of ML
What 


When 
May 11, 2015 from 04:00 PM to 05:00 PM 
Where  IF 2.33 
Add event to calendar 
vCal iCal 
Abstract:
I will present the CakeML project. This project centres around a
subset of ML that is carefully chosen to be easy to write programs
in and convenient to reason about formally. I will talk about
results so far, in particular, our a formally verified
implementation of CakeML (a compiler and a readevalprint loop) in
64bit x86 machine code. The construction and verification of this
implementation required both proofs of highlevel programs (the
parser, type inferencer and compiler) and lowlevel programs (the
runtime in x86 machine code, its bignum library and garbage
collector). We used a novel technique to produce much of the
verified lowlevel code: we bootstrapped the verified compiler
algorithm, within higherorder logic, to produce the verified
lowlevel implementation. We proved divergence preservation using
simple clocks. This work was carried out using the HOL4 theorem
prover and is a collaborative effort, where the main contributors
are Ramana Kumar, Magnus Myreen, Michael Norrish and Scott Owens.