CakeML: A Verified Implementation of ML

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

• Ramana Kumar (University of Cambridge)
• Tuesday 03 December 2013, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.