The VLISP verified Scheme system

William Clinger. The Scheme 311 compiler: An exercise in denotational semantics. In1984 ACM Symposium on Lisp and Functional Programming, pages 356?364, New York, August 1984. The Association for Computing Machinery, Inc.

William M. Farmer. A partial functions version of Church's simple theory of types.Journal of Symbolic Logic, 55(3):1269?91, 1990. Also MITRE Corporation technical report M88-52, 1988; revised 1990.

William M. Farmer, Joshua D. Guttman, Leonard G. Monk, John D. Ramsdell, and Vipin Swarup. The faithfulness of the VLISP operational semantics. M 92B093, The MITRE Corporation, September 1992.

William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. IMPS: an Interactive Mathematical Proof System.Journal of Automated Reasoning, 11(2):213?248, October 1993.

Joshua D. Guttman, Leonard G. Monk, William M. Farmer, John D. Ramsdell, and Vipin Swarup. The VLISP byte-code compiler. M 92B092, The MITRE Corporation, September 1992.

Joshua D. Guttman, Leonard G. Monk, William M. Farmer, John D. Ramsdell, and Vipin Swarup. The VLISP flattener. M. 92B094, The MITRE Corporation, 1992.

Joshua D. Guttman, John D. Ramsdell, and Mitchell Wand. VLISP: A verified implementation of Scheme.Lisp and Symbolic Computation, 8(1/2):5?32, 1995.

C. A. R. Hoare. Notes on data structuring. In O.-J. Dahl, editor,Structured Programming. Academic Press, 1972.

IEEE Std 1178?1990.IEEE Standard for the Scheme Programming Language. Institute of Electrical and Electronic Engineers, Inc., New York, NY, 1991.

Richard A. Kelsey and Jonathan A. Rees. Scheme48 progress report. Manuscript in preparation, 1992.

Richard A. Kelsey and Jonathan A. Rees. A tractable Scheme implementation.Lisp and Symbolic Computation, 7(4):315?335, 1994.

Robin Milner.Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.

Dino P. Oliva, John D. Ramsdell, and Mitchell Wand. The VLISP verified PreScheme compiler.Lisp and Symbolic Computation, 8(1/2):111?182, 1995.

John D. Ramsdell. The revised VLISP PreScheme front end. M 93B095, The MITRE Corporation, August 1993.

Jonathan A. Rees, Norman I. Adams, and James R. Meehan.The T Manual. Computer Science Department, Yale University, fifth edition edition, 1988.

Joseph E. Stoy.Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, MA, 1977.

Vipin Swarup, William M. Farmer, Joshua D. Guttman, Leonard G. Monk, and John D. Ramsdell. The VLISP byte-code interpreter. M 92B097, The MITRE Corporation, September 1992.

Mitchell Wand. Semantics-directed machine architecture. InConf. Rec. 9th ACM Symp. on Principles of Prog. Lang., pages 234?241, 1982.

Mitchell Wand and Dino P. Oliva. Proving the correctness of storage representations. InProceedings of the 1992 ACM Conference on Lisp and Functional Programming, pages 151?160, New York, 1992. ACM Press.