@InProceedings{nondetcalc,
  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,
  Date = {2015-06-09},
  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
\emph{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 \emph{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,Rocq, program calculation},
  Url = {http://dx.doi.org/10.1007/978-3-319-19797-5_8}
}