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

29 views
Skip to first unread message

Patrik Jansson

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

/Patrik


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

andrea...@gu.se
http://www2.tcs.ifi.lmu.de/~abel/
_______________________________________________
Proglog mailing list
Pro...@lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/proglog



--
Patrik Jansson, Professor of Computer Science, 
Head of Division, Software Technology, 
Department of Computer Science and Engineering,
Chalmers U. of Tech. & U. of Gothenburg
https://www.chalmers.se/cse/EN/people/jansson-patrik

Reply all
Reply to author
Forward
0 new messages