No Subject

   The Verified Programming Language Implementation project
   has developed a formally verified implementation of the Scheme
   programming language, called Vlisp.  The contributors were Joshua D.
   Guttman, John D.  Ramsdell, William M. Farmer, Leonard G. Monk,
   and Vipin Swarup, of The MITRE Corporation, and Mitchell Wand and
   Dino Oliva of Northeastern University.

   An overview of the project is presented in the Vlisp Guide.

enjoy...	oz
---
ps: as an internetworking courtesy, please, try to avoid ftp
    transfers during peak working hours, i.e. 9am to 5pm EST.
---
vlisp papers: filenames and bibliographic details:
   
pureprescheme.dvi
   Dino P. Oliva and Mitchell Wand.
   A Verified Compiler for Pure PreScheme.
   Northeastern University College of Computer Science
   Technical Report NU-CCS-92-5,
   Feb 1992.
   
runtime.dvi
   Dino P. Oliva and Mitchell Wand.
   A Verified Runtime Structure for Pure PreScheme.
   Northeastern University College of Computer Science
   Technical Report NU-CCS-92-27.
   Sep 1992.
   
guide.dvi
   J. D. Guttman, L. G. Monk, J. D. Ramsdell, W. M. Farmer and V. Swarup.
   A Guide to vlisp, A Verified Programming Language Implementation
   Technical Report M92B091, The MITRE Corporation.
   Sep 1992.
   
compiler.dvi
   J. D. Guttman, L. G. Monk, W. M. Farmer, J. D. Ramsdell and V. Swarup.
   The vlisp Byte-Code Compiler.
   Technical Report M92B092, The MITRE Corporation.
   Sep. 1992.
   
faithfullness.dvi
   W. M. Farmer, J. D. Guttman, L. G. Monk, J. D. Ramsdell and V. Swarup.
   The Faithfulness of the vlisp Operational Semantics.
   Technical REport M92B093, The MITRE Corporation.
   Sep. 1992.
   
flattener.dvi
   J. D. Guttman, L. G. Monk, W. M. Farmer, J. D. Ramsdell and V. Swarup.
   The vlisp Flattener.
   Technical Report M92B094, The MITRE Corporation.
   Sep. 1992.
   
linker.dvi
   W. M. Farmer, J. D. Guttman, L. G. Monk, J. D. Ramsdell and V. Swarup.
   The vlisp Linker.
   Technical Report M92B095, The MITRE Corporation.
   Sep 1992.
   
image_builder.dvi
   V. Swarup, W. M. Farmer, J. D. Guttman, L. G. Monk and J. D. Ramsdell.
   The vlisp Image Builder.
   Technical Report M92B096, The MITRE Corporation.
   Sep 1992.
   
vm.dvi
   V. Swarup, W. M. Farmer, J. D. Guttman, L. G. Monk and J. D. Ramsdell.
   The vlisp Byte-Code Interpreter.
   Technical Report M92B097, The MITRE Corporation.
   Sep 1992.
   
prescheme.dvi
   J. D. Ramsdell, W. M. Farmer, J. D. Guttman, L. G. Monk and V. Swarup.
   The vlisp PreScheme Front End.
   Technical Report M92B098, The MITRE Corporation.
   Sep 1992.