A new verified compiler backend for CakeML

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

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
ICFP 2016
Nara, Japan
Association for Computing Machinery
New York, NY, USA
Pages 60-73
2016
Note(s): ISA specification, Verified compilers, CakeML compiler, x86 architecture, Arm architecture, RISCV architecture, MIPS architecture