Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS seminar : Magnus Myreen: CakeML: a formally verified implementation of ML

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

— filed under:

What
  • LFCS Seminar
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 read-eval-print loop) in
64-bit x86 machine code. The construction and verification of this
implementation required both proofs of high-level programs (the
parser, type inferencer and compiler) and low-level programs (the
runtime in x86 machine code, its bignum library and garbage
collector). We used a novel technique to produce much of the
verified low-level code: we bootstrapped the verified compiler
algorithm, within higher-order logic, to produce the verified
low-level 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.

Document Actions