CakeML: A verified implementation of ML

Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens
[doi] [Google Scholar] [DBLP] [Citeseer]

Principles of Programming Languages (POPL)
ACM
Pages 179-192
2014

Verified compilers