LISP and Symbolic Computation, 8(1/2)5-32
VLISP: A Verified Implementation of SchemeJoshua D. Guttman, The MITRE Corporation, 202 Burlington Road, Bedford, MA 01730-1420
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: The VLISP project showed how to produce a
comprehensively verified implementation for a programming language,
namely Scheme. This paper introduces two more detailed studies on
VLISP [13, 21]. It summarizes the basic techniques that were used
repeatedly throughout the effort. It presents scientific conclusions
about the applicability of these techniques as well as engineering
conclusions about the crucial choices that allowed the verification to
succeed. Keywords: verified, programming languages, Scheme, compiler |
[local copy]
![[picture of journal cover]](../LISP.JPG)