A kripke logical relation between ML and assembly
2011pp. 133–146
Citations Over TimeTop 10% of 2011 papers
Abstract
There has recently been great progress in proving the correctness of compilers for increasingly realistic languages with increasingly realistic runtime systems. Most work on this problem has focused on proving the correctness of a particular compiler, leaving open the question of how to verify the correctness of assembly code that is hand-optimized or linked together from the output of multiple compilers. This has led Benton and other researchers to propose more abstract, compositional notions of when a low-level program correctly realizes a high-level one. However, the state of the art in so-called "compositional compiler correctness" has only considered relatively simple high-level and low-level languages.
Related Papers
- → Verification of Compilers(1999)62 cited
- Operational refinement for compiler correctness(2012)
- → Construction of Verified Compiler Front-Ends with Program-Checking(2000)16 cited
- → Bringing extensibility to verified compilers(2010)2 cited
- → Using domain algebras to prove the correctness of a compiler(2005)23 cited