Calculating Certified Compilers for Non-deterministic Languages

    Research output: Conference Article in Proceeding or Book/Report chapterBook chapterResearchpeer-review

    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.
    Original languageUndefined/Unknown
    Title of host publicationMathematics of Program Construction
    EditorsRalf Hinze, Janis Voigtländer
    Number of pages28
    Volume9129
    PublisherSpringer
    Publication date1 Jun 2015
    Pages159-186
    ISBN (Print)978-3-319-19796-8
    DOIs
    Publication statusPublished - 1 Jun 2015

    Keywords

    • compiler, verification,coq, program calculation

    Cite this