University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > CakeML: A Verified Implementation of ML

CakeML: A Verified Implementation of ML

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact William Denman.

(A practice talk for POPL 2014 . 25 mins max.)

We have verified and bootstrapped a compiler for a large subset of standard ML. The resulting system, CakeML, is a read-eval-print loop implemented in x86-64 machine code and proved correct (in higher-order logic) with respect to our semantics for ML and for x86-64.

This is the first verification of compiler bootstrapping, which we use to automate much of the synthesis and verification of the compiler’s implementation in machine code. The verification depends on a tiny trusted code base (a HOL proof checker), and covers lexing, parsing, type inference, dynamic and incremental compilation, garbage collection and bignum arithmetic. We have proved semantics-preservation including divergence-preservation. For the latter we use a novel lightweight method based on logical timeouts.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity