Volume 8, Numbers 1/2, 1995 Special Issue on VLISP, Guest Editors: Joshua D. Gutman and Mitchell Wand. LISP AND SYMBOLIC COMPUTATION: An International Journal 8, 5–32 (1995) © 1995 Kluwer Academic Publishers. Manufactured in The Netherlands. # VLISP: A Verified Implementation of Scheme JOSHUA D. GUTTMAN JOHN D. RAMSDELL The MITRE Corporation, 202 Burlington Road, Bedford, MA 01730-1420 guttman@mitre.org ramsdell@mitre.org MITCHELL WAND College of Computer Science, 161 Cullinane Hall, Northeastern University, Boston, MA 02115 wand@ccs.neu.edu Editors: Joshua D. Guttman and Mitchell Wand ## 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 LISP AND SYMBOLIC COMPUTATION: An International Journal 8, 33–110 (1995) © 1995 Kluwer Academic Publishers. Manufactured in The Netherlands. ## The VLISP Verified Scheme System JOSHUA D. GUTTMAN JOHN D. RAMSDELL VIPIN SWARUP The MITRE Corporation, 202 Burlington Road, Bedford, MA 01730-1420 guttman@mitre.org ramsdell@mitre.org swarup@mitre.org Editors: Joshua D. Guttman and Mitchell Wand ## 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 LISP AND SYMBOLIC COMPUTATION: An International Journal 8, 111–Volume 8, Numbers 1/2, 1995 Special Issue on VLISP, Guest Editors: Joshua D. Gutman and Mitchell Wand. LISP AND SYMBOLIC COMPUTATION: An International Journal 8, 5–32 (1995) © 1995 Kluwer Academic Publishers. Manufactured in The Netherlands. # VLISP: A Verified Implementation of Scheme JOSHUA D. GUTTMAN JOHN D. RAMSDELL The MITRE Corporation, 202 Burlington Road, Bedford, MA 01730-1420 guttman@mitre.org ramsdell@mitre.org MITCHELL WAND College of Computer Science, 161 Cullinane Hall, Northeastern University, Boston, MA 02115 wand@ccs.neu.edu Editors: Joshua D. Guttman and Mitchell Wand ## 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 LISP AND SYMBOLIC COMPUTATION: An International Journal 8, 33–110 (1995) © 1995 Kluwer Academic Publishers. Manufactured in The Netherlands. ## The VLISP Verified Scheme System JOSHUA D. GUTTMAN JOHN D. RAMSDELL VIPIN SWARUP The MITRE Corporation, 202 Burlington Road, Bedford, MA 01730-1420 guttman@mitre.org ramsdell@mitre.org swarup@mitre.org Editors: Joshua D. Guttman and Mitchell Wand ## 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 LISP AND SYMBOLIC COMPUTATION: An International Journal 8, 111–