Verified compilation of CakeML to multiple machine-code targets

Anthony Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer] [url]

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs
CPP 2017
Paris, France
Association for Computing Machinery
New York, NY, USA
Pages 125-137
Note(s): ISA specification, Verified compilers, CakeML compiler