CORRECTNESS OF A COMPILER SPECIFICATION FOR THE SECD MACHINE

Abstract

We develop a specification in Natural Semantics of a compiler from the lambda calculus with let and letrec (miniSML) to the SECD machine. We prove that the compiler specification is correct by simplifying the approach of Despeyroux [2] and changing the proof technique to work with non-terminating semantics. We then extend the SECD to handle lazy evaluation and outline the proof of the compiler specification for this.