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
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
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-patrikReply all
Reply to author
Forward
0 new messages