@Article{OlivaRamsdellWand95,
  author = 	"Dino P. Oliva and John D. Ramsdell and Mitchell Wand",
  title = 	"The VLISP Verified PreScheme Compiler",
  journal = 	"Lisp and Symbolic Computation",
  year = 	"1995",
  URL = {ftp://ftp.ccs.neu.edu/pub/people/wand/vlisp/lasc/prescheme.dvi},
  volume = 	"8",
  number = 	"1/2",
  pages = 	"111-182",
  abstract =   "This paper describes a verified compiler for PreScheme, the
implementation language for the {\vlisp} run-time system.  The
compiler and proof were divided into three parts: A transformational
front end that translates source text into a core language, a
syntax-directed compiler that translates the core language into
combinator-based tree-manipulation language, and a linearizer that
translates combinator code into code for an abstract stored-program
machine with linear memory for both data and code.  This factorization
enabled different proof techniques to be used for the different phases
of the compiler, and also allowed the generation of good
code. Finally, the whole process was made possible by carefully
defining the semantics of {\vlisp} PreScheme rather than just
adopting Scheme's.  We believe that the architecture of the compiler
and its correctness proof can easily be applied to compilers for
languages other than PreScheme."
}

{"_id":"fKNAw7HWc39pKecfY","bibbaseid":"oliva-ramsdell-wand-thevlispverifiedpreschemecompiler-1995","downloads":0,"creationDate":"2017-04-23T20:31:12.577Z","title":"The VLISP Verified PreScheme Compiler","author_short":["Oliva, D. P.","Ramsdell, J. D.","Wand, M."],"year":1995,"bibtype":"article","biburl":"http://www.ccs.neu.edu/home/wand/Bibliography.bib","bibdata":{"bibtype":"article","type":"article","author":[{"firstnames":["Dino","P."],"propositions":[],"lastnames":["Oliva"],"suffixes":[]},{"firstnames":["John","D."],"propositions":[],"lastnames":["Ramsdell"],"suffixes":[]},{"firstnames":["Mitchell"],"propositions":[],"lastnames":["Wand"],"suffixes":[]}],"title":"The VLISP Verified PreScheme Compiler","journal":"Lisp and Symbolic Computation","year":"1995","url":"ftp://ftp.ccs.neu.edu/pub/people/wand/vlisp/lasc/prescheme.dvi","volume":"8","number":"1/2","pages":"111-182","abstract":"This paper describes a verified compiler for PreScheme, the implementation language for the ľisp run-time system. The compiler and proof were divided into three parts: A transformational front end that translates source text into a core language, a syntax-directed compiler that translates the core language into combinator-based tree-manipulation language, and a linearizer that translates combinator code into code for an abstract stored-program machine with linear memory for both data and code. This factorization enabled different proof techniques to be used for the different phases of the compiler, and also allowed the generation of good code. Finally, the whole process was made possible by carefully defining the semantics of ľisp PreScheme rather than just adopting Scheme's. We believe that the architecture of the compiler and its correctness proof can easily be applied to compilers for languages other than PreScheme.","bibtex":"@Article{OlivaRamsdellWand95,\n author = \t\"Dino P. Oliva and John D. Ramsdell and Mitchell Wand\",\n title = \t\"The VLISP Verified PreScheme Compiler\",\n journal = \t\"Lisp and Symbolic Computation\",\n year = \t\"1995\",\n URL = {ftp://ftp.ccs.neu.edu/pub/people/wand/vlisp/lasc/prescheme.dvi},\n volume = \t\"8\",\n number = \t\"1/2\",\n pages = \t\"111-182\",\n abstract = \"This paper describes a verified compiler for PreScheme, the\nimplementation language for the {\\vlisp} run-time system. The\ncompiler and proof were divided into three parts: A transformational\nfront end that translates source text into a core language, a\nsyntax-directed compiler that translates the core language into\ncombinator-based tree-manipulation language, and a linearizer that\ntranslates combinator code into code for an abstract stored-program\nmachine with linear memory for both data and code. This factorization\nenabled different proof techniques to be used for the different phases\nof the compiler, and also allowed the generation of good\ncode. Finally, the whole process was made possible by carefully\ndefining the semantics of {\\vlisp} PreScheme rather than just\nadopting Scheme's. We believe that the architecture of the compiler\nand its correctness proof can easily be applied to compilers for\nlanguages other than PreScheme.\"\n}\n\n","author_short":["Oliva, D. P.","Ramsdell, J. D.","Wand, M."],"key":"OlivaRamsdellWand95","id":"OlivaRamsdellWand95","bibbaseid":"oliva-ramsdell-wand-thevlispverifiedpreschemecompiler-1995","role":"author","urls":{"Paper":"ftp://ftp.ccs.neu.edu/pub/people/wand/vlisp/lasc/prescheme.dvi"},"downloads":0,"html":""},"search_terms":["vlisp","verified","prescheme","compiler","oliva","ramsdell","wand"],"keywords":[],"authorIDs":["58fd0f10bfc623c939000018"],"dataSources":["zM8mNPR4ZkAHKtvDs"]}