Skip to main content
SpringerLink
Log in

The VLISP verified Scheme system

  • Published:
LISP and Symbolic Computation

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. 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.

    Google Scholar 

  2. 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.

    Google Scholar 

  3. 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.

  4. 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.

    Google Scholar 

  5. 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.

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

  7. 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.

    Google Scholar 

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

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

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

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

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

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

    Google Scholar 

  17. 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.

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

  19. 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.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. The MITRE Corporation, 202 Burlington Road, 01730-1420, Bedford, MA

    Joshua D. Guttman, John D. Ramsdell & Vipin Swarup

Authors
  1. Joshua D. Guttman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. John D. Ramsdell
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Vipin Swarup
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

The work reported here was carried out as part of The MITRE Corporation's Technology Program, under funding from Rome Laboratory, Electronic Systems Command, United States Air Force, through contract F19628-89-C-0001. Preparation of this paper was generously supported by The MITRE Corporation.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Guttman, J.D., Ramsdell, J.D. & Swarup, V. The VLISP verified Scheme system. Lisp and Symbolic Computation 8, 33–110 (1995). https://doi.org/10.1007/BF01128407

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01128407

Keywords

Search

Navigation