Abstract

We present an approach to compiler implementation using Oliveira and Cook's structured graphs that avoids the use of explicit labels and jumps in the generated intermediate code. The use of structured graphs significantly simplifies reasoning over the generated code while retaining the expressive power of explicit jumps. By virtue of its simplicity, our method is particularly suited for compiler calculation, a technique that derives a compiler implementation from a language semantics by means of formal calculations.

Categories: Compilers, Formal Verification

Tags: Graphs, Higher-order Abstract Syntax, Compiler, Virtual Machine, Calculation, Constructive Induction, Defunctionalisation, Contiuation-passing Style