Verified compilers

[Google Scholar]

Notes: CompCert compiler, CakeML compiler
Papers: samet:ieeetse:1977, samet:phd:1975, leroy:cacm:2009, kumar:popl:2014

CompCert compiler

  • Verified compilation of CakeML to multiple machine-code targets [fox:cpp:2017]
  • Formal verification of a realistic compiler [leroy:cacm:2009]
  • CompCertTSO: A verified compiler for relaxed-memory concurrency [sevcik:jacm:2013]
  • A new verified compiler backend for CakeML [tan:icfp:2016]