Fwd: [Proglog] Wed Feb 25 13:15 Magnus Myreen, ''CakeML: a formally verified compiler for ML''

Skip to first unread message

Patrik Jansson

Feb 22, 2015, 4:33:45 PM2/22/15
to af...@googlegroups.com
For those interested there will be an AFP-related research talk by Magnus Myreen on Wednesday. See details below.


---------- 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.

  Magnus Myreen

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

Patrik Jansson, Professor of Computer Science, 
Head of Division, Software Technology, 
Department of Computer Science and Engineering,
Chalmers U. of Tech. & U. of Gothenburg

Reply all
Reply to author
0 new messages