TY - GEN
T1 - Calculating certified compilers for non-deterministic languages
AU - Bahr, Patrick
PY - 2015
Y1 - 2015
N2 - Reasoning about programming languages with nondeterministic semantics entails many difficulties. For instance, to prove correctness of a compiler for such a language, one typically has to split the correctness property into a soundness and a completeness part, and then prove these two parts separately. In this paper, we present a set of proof rules to prove compiler correctness by a single proof in calculational style. The key observation that led to our proof rules is the fact that the soundness and completeness proof follow a similar pattern with only small differences. We condensed these differences into a single side condition for one of our proof rules. This side condition, however, is easily discharged automatically by a very simple form of proof search. We implemented this calculation framework in the Coq proof assistant. Apart from verifying a given compiler, our proof technique can also be used to formally derive – from the semantics of the source language – a compiler that is correct by construction. For such a derivation to succeed it is crucial that the underlying correctness argument proceeds as a single calculation, as opposed to separate calculations of the two directions of the correctness property. We demonstrate our technique by deriving a compiler for a simple language with interrupts.
AB - Reasoning about programming languages with nondeterministic semantics entails many difficulties. For instance, to prove correctness of a compiler for such a language, one typically has to split the correctness property into a soundness and a completeness part, and then prove these two parts separately. In this paper, we present a set of proof rules to prove compiler correctness by a single proof in calculational style. The key observation that led to our proof rules is the fact that the soundness and completeness proof follow a similar pattern with only small differences. We condensed these differences into a single side condition for one of our proof rules. This side condition, however, is easily discharged automatically by a very simple form of proof search. We implemented this calculation framework in the Coq proof assistant. Apart from verifying a given compiler, our proof technique can also be used to formally derive – from the semantics of the source language – a compiler that is correct by construction. For such a derivation to succeed it is crucial that the underlying correctness argument proceeds as a single calculation, as opposed to separate calculations of the two directions of the correctness property. We demonstrate our technique by deriving a compiler for a simple language with interrupts.
U2 - 10.1007/978-3-319-19797-5_8
DO - 10.1007/978-3-319-19797-5_8
M3 - Article in proceedings
AN - SCOPUS:84937510940
SN - 978-3-319-19796-8
T3 - Lecture notes in computer science
SP - 159
EP - 186
BT - Mathematics of program construction
A2 - Hinze, Ralf
A2 - Voigtländer, Janis
PB - Springer
T2 - 12th International Conference on Mathematics of Program Construction, MPC 2015
Y2 - 29 June 2015 through 1 July 2015
ER -