A COMPILER CORRECTNESS PROOF FOR THE STATIC LINK TECHNIQUE BY MEANS OF EVOLVING ALGEBRAS
Markus Mohnen · Fundamenta Informaticae · 1997
The well-known static link technique is used for stack-based implementations of imperative programming languages which admit nested recursive procedure declarations. Its basic idea is to access non-local variables by tracing a static link chain to lower stack elements. Evolving algebras are a new method for defining operational semantics of abstract machines. Based on an appropriate stack machine, defined as an evolving algebra, and a functional description of a compiler for a sample language, we give a complete proof of correctness for this technique using the method of refinement.