CakeML: a verified implementation of ML.

Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens

Browse the full POPL paper archive.