Please use this identifier to cite or link to this item:
|Title:||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  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.|
|Appears in Collections:||Technical Reports|
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.