Proving Correctness of Compilers Using Structured Graphs

Research output: Conference Article in Proceeding or Book/Report chapterBook chapterResearchpeer-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.
Original languageUndefined/Unknown
Title of host publicationFunctional and Logic Programming
EditorsMichael Codish, Eijiro Sumii
Number of pages17
Volume8475
PublisherSpringer International Publishing, Switzerland
Publication date1 Jun 2014
Pages221-237
ISBN (Print)978-3-319-07150-3
DOIs
Publication statusPublished - 1 Jun 2014

Keywords

  • compiler,verification,graphs,fold,free monad

Cite this