Proving Correctness of Compilers Using Structured Graphs

    Publikation: Konference artikel i Proceeding eller bog/rapport kapitelBidrag til bog/antologiForskningpeer review

    Abstract

    We present an approach to compiler implementation using Oliveira and Cook’s structured graphs that avoids the use of explicit jumps in the generated code. The advantage of our method is that it takes the implementation of a compiler using a tree type along with its correctness proof and turns it into a compiler implementation using a graph type along with a correctness proof. The implementation and correctness proof of a compiler using a tree type without explicit jumps is simple, but yields code duplication. Our method provides a convenient way of improving such a compiler without giving up the benefits of simple reasoning.
    OriginalsprogUdefineret/Ukendt
    TitelFunctional and Logic Programming
    RedaktørerMichael Codish, Eijiro Sumii
    Antal sider17
    Vol/bind8475
    ForlagSpringer International Publishing, Switzerland
    Publikationsdato1 jun. 2014
    Sider221-237
    ISBN (Trykt)978-3-319-07150-3
    DOI
    StatusUdgivet - 1 jun. 2014

    Emneord

    • compiler,verification,graphs,fold,free monad

    Citationsformater