LISP and Symbolic Computation, 8(1/2)111-182
The VLISP Verified PreScheme CompilerDino P. Oliva, College of Computer Science, 161 Cullinane Hall, Northeastern University, Boston, MA 02115
John D. Ramsdell, The MITRE Corporation, 202 Burlington Road, Bedford, MA 01730-1420
Mitchell Wand, College of Computer Science, 161 Cullinane Hall, Northeastern University, Boston, MA 02115
|
Abstract: This paper describes a verified compiler for
PreScheme, the implementation language for the VLISP run-time
system. The compiler and proof were divided into three parts: A
transformational front end that translates source text into a core
language, a syntax-directed compiler that translates the core language
into a combinator-based treemanipulation language, and a linearizer
that translates combinator code into code for an abstract
stored-program machine with linear memory for both data and code. This
factorization enabled different proof techniques to be used for the
different phases of the compiler, and also allowed the generation of
good code. Finally, the whole process was made possible by carefully
defining the semantics of VLISP PreScheme rather than just adopting
Scheme's. We believe that the architecture of the compiler and its
correctness proof can easily be applied to compilers for languages
other than PreScheme. Keywords: verified, compiler |
[local copy]
![[picture of journal cover]](../LISP.JPG)