@InProceedings{bahr15mpc,
Title = {Calculating Certified Compilers for Non-deterministic Languages},
Author = {Patrick Bahr},
Booktitle = {Mathematics of Program Construction},
Year = {2015},
Editor = {Hinze, Ralf and VoigtlĂ¤nder, Janis},
Month = jun,
Pages = {159-186},
Publisher = {Springer International Publishing},
Series = {Lecture Notes in Computer Science},
Volume = {9129},
Abstract = {Reasoning about programming languages with non-deterministic
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 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.},
Doi = {10.1007/978-3-319-19797-5_8},
ISBN = {978-3-319-19796-8},
Keywords = {compiler, verification,coq, program calculation},
Url = {http://dx.doi.org/10.1007/978-3-319-19797-5_8}
}