Calculating certified compilers for non-deterministic languages
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
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.
Originalsprog | Engelsk |
---|---|
Titel | Mathematics of program construction : 12th International Conference, MPC 2015, Königswinter, Germany, June 29--July 1, 2015. Proceedings |
Redaktører | Ralf Hinze, Janis Voigtländer |
Antal sider | 28 |
Forlag | Springer |
Publikationsdato | 2015 |
Sider | 159-186 |
ISBN (Trykt) | 978-3-319-19796-8 |
ISBN (Elektronisk) | 978-3-319-19797-5 |
DOI | |
Status | Udgivet - 2015 |
Begivenhed | 12th International Conference on Mathematics of Program Construction, MPC 2015 - Konigswinter, Tyskland Varighed: 29 jun. 2015 → 1 jul. 2015 |
Konference
Konference | 12th International Conference on Mathematics of Program Construction, MPC 2015 |
---|---|
Land | Tyskland |
By | Konigswinter |
Periode | 29/06/2015 → 01/07/2015 |
Navn | Lecture notes in computer science |
---|---|
Vol/bind | 9129 |
ISSN | 0302-9743 |
ID: 159747597