LISP and Symbolic Computation, 8(1/2)33-110
The VLISP Verified Scheme SystemJoshua 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
Vipin Swarup, The MITRE Corporation, 202 Burlington Road, Bedford, MA 01730-1420
|
Abstract: The VLISP project has produced a rigorously verified
compiler from Scheme to byte codes, and a verified interpreter for the
resulting byte codes. The official denotational semantics for Scheme
provides the main criterion of correctness. The Wand-Clinger technique
was used to prove correctness of the primary compiler step. Then a
state machine operational semantics is proved to be faithful to the
denotational semantics. The remainder of the implementation is
verified by a succession of state machine refinement proofs. These
include proofs that garbage collection is a sound implementation
strategy, and that a particular garbage collection algorithm is
correct. Keywords: Scheme, verified, compiler, interpreter, denotational semantics, operational semantics, refinement, garbage collection |
[local copy]
![[picture of journal cover]](../LISP.JPG)