Conference paper
Provably correct compiler development and implementation
This paper reports on provably correct compiler implementation in the ESPRIT basic research action 3104 ProCoS (Provably Correct Systems). A sharp distinction is drawn between correctness of the specification of a compiler and correctness of the actual implementation. The first covers semantical correctness of the code to be generated, whereas the second concerns correctness of the compiler program with respect to the specification.
The compiler construction framework presented aims at minimizing the amount of handcoding during implementation and at reusing specification correctness arguments for proving the implementation correct. The classical technique of bootstrapping compilers is revisited with respect to implementation correctness.
Language: | English |
---|---|
Publisher: | Springer Verlag |
Year: | 1992 |
Pages: | 141-155 |
Proceedings: | Compiler Construction |
ISBN: | 3540473351 , 3540559841 , 9783540473350 and 9783540559849 |
Types: | Conference paper |
DOI: | 10.1007/3-540-55984-1_14 |