---------- Forwarded message ----------
From: Andreas Abel <ab...@chalmers.se>
Date: 2015-02-18 23:14 GMT+01:00
Subject: [Proglog] Wed Feb 25 13:15 Magnus Myreen, ''CakeML: a formally verified compiler for ML''
To: ProgLog <pro...@lists.chalmers.se
Welcome to the ProgLog seminar on Wednesday, February 25 at 1.15 pm in room 8103.
will talk about
CakeML: a formally verified compiler for ML
Abstract: I will present the CakeML project. This project centers 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 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. I will also explain how divergence preservation was proved using simple clocks. This work was carried out using the HOL4 theorem prover.
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
Proglog mailing list