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

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

CakeML: A Verified Implementation of ML

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

MRC Cognition & Brain Sciences Unit, 15 Chaucer Road, Cambridge CB2 7EF Hero Alam Zoom link

Other talks

Title to be confirmed Tissue-scale communication in cancer development TBC Cambridge RNA Club - IN PERSON Title TBC title abstract tbc
 

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