Proving the Correctness of the Static Link Technique Using Evolving
Algebras

M. Mohnen

           The {\em static link technique\/} is used for the stack-based
           implementation of imperative programming languages which admit
           nested recursive procedure declarations. It was suggested
           in 1960 by Dijkstra as an extension of the stack technique
           for the evaluation of expressions. Its basic idea is to
           access global variables by tracing a static link chain to
           lower stack elements.  {\em Evolving algebras\/} are a new
           method for the definition of 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 will give a complete proof of this
           technique.  Especially, we will transform the evolving algebra
           for the stack machine into a more abstract one, i.e., into
           a new machine which is closer to the denotational semantics
           of the sample language.