Please use this identifier to cite or link to this item: http://hdl.handle.net/1880/46525
Title: CORRECTNESS OF A COMPILER SPECIFICATION FOR THE SECD MACHINE
Authors: Simpson, Todd
Keywords: Computer Science
Issue Date: 1-Oct-1990
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.
URI: http://hdl.handle.net/1880/46525
Appears in Collections:Technical Reports

Files in This Item:
File Description SizeFormat 
1990-410-34.pdf3.86 MBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.