Calculating certified compilers for non-deterministic languages
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
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.
Original language | English |
---|---|
Title of host publication | Mathematics of program construction : 12th International Conference, MPC 2015, Königswinter, Germany, June 29--July 1, 2015. Proceedings |
Editors | Ralf Hinze, Janis Voigtländer |
Number of pages | 28 |
Publisher | Springer |
Publication date | 2015 |
Pages | 159-186 |
ISBN (Print) | 978-3-319-19796-8 |
ISBN (Electronic) | 978-3-319-19797-5 |
DOIs | |
Publication status | Published - 2015 |
Event | 12th International Conference on Mathematics of Program Construction, MPC 2015 - Konigswinter, Germany Duration: 29 Jun 2015 → 1 Jul 2015 |
Conference
Conference | 12th International Conference on Mathematics of Program Construction, MPC 2015 |
---|---|
Land | Germany |
By | Konigswinter |
Periode | 29/06/2015 → 01/07/2015 |
Series | Lecture notes in computer science |
---|---|
Volume | 9129 |
ISSN | 0302-9743 |
ID: 159747597