Advice on structuring compilers and proving them correct
1973pp. 144–152
Citations Over TimeTop 10% of 1973 papers
Abstract
The purpose of this paper is to advise an approach (and to support that advice by discussion of an example) towards achieving a goal first announced by John McCarthy: that compilers for higher-level programming languages should be made completely trustworthy by proving their correctness. The author believes that the compiler-correctness problem can be made much less general and better-structured than the unrestricted program-correctness problem; to do so will of course entail restricting what a compiler may be.
Related Papers
- → Verification of Compilers(1999)62 cited
- → Advice on structuring compilers and proving them correct(1973)129 cited
- Operational refinement for compiler correctness(2012)
- → Construction of Verified Compiler Front-Ends with Program-Checking(2000)16 cited
- Compiler System for Visual Programming Language(2007)