CORRECTNESS OF A COMPILER SPECIFICATION FOR THE SECD MACHINE
Date
1990-10-01
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
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.
Description
Keywords
Computer Science