A Verified Compiler for Pure PreScheme. Oliva, D. P. & Wand, M. Technical Report NU-CCS-92-5, Northeastern University College of Computer Science, February, 1992. abstract bibtex This document gives a summary of activities under MITRE Contract Number F19628-89-C-001. It gives a detailed denotational specification of the language Pure PreScheme. A bytecode compiler, derived from the semantics, is presented, followed by proofs of correctness of the compiler with respect to the semantics. Finally, an assembler from the bytecode to an actual machine architecture is shown.
@TechReport{OlivaWand92,
author = "Dino P. Oliva and Mitchell Wand",
title = "A Verified Compiler for Pure PreScheme",
institution = "Northeastern University College of Computer Science",
year = "1992",
type = "Technical Report",
number = "NU-CCS-92-5",
OPTaddress = "",
month = feb,
OPTnote = "",
abstract = "This document gives a summary of activities under
MITRE Contract Number F19628-89-C-001. It gives a
detailed denotational specification of the language
Pure Pre\-Scheme. A bytecode compiler, derived from
the semantics, is presented, followed by proofs of
correctness of the compiler with respect to the
semantics. Finally, an assembler from the bytecode
to an actual machine architecture is shown."
}
Downloads: 0
{"_id":"KjR8Z7SuDRgb7XuLC","bibbaseid":"oliva-wand-averifiedcompilerforpureprescheme-1992","downloads":0,"creationDate":"2017-04-23T20:31:12.566Z","title":"A Verified Compiler for Pure PreScheme","author_short":["Oliva, D. P.","Wand, M."],"year":1992,"bibtype":"techreport","biburl":"http://www.ccs.neu.edu/home/wand/Bibliography.bib","bibdata":{"bibtype":"techreport","type":"Technical Report","author":[{"firstnames":["Dino","P."],"propositions":[],"lastnames":["Oliva"],"suffixes":[]},{"firstnames":["Mitchell"],"propositions":[],"lastnames":["Wand"],"suffixes":[]}],"title":"A Verified Compiler for Pure PreScheme","institution":"Northeastern University College of Computer Science","year":"1992","number":"NU-CCS-92-5","optaddress":"","month":"February","optnote":"","abstract":"This document gives a summary of activities under MITRE Contract Number F19628-89-C-001. It gives a detailed denotational specification of the language Pure PreScheme. A bytecode compiler, derived from the semantics, is presented, followed by proofs of correctness of the compiler with respect to the semantics. Finally, an assembler from the bytecode to an actual machine architecture is shown.","bibtex":"@TechReport{OlivaWand92,\n author = \t\"Dino P. Oliva and Mitchell Wand\",\n title = \t\"A Verified Compiler for Pure PreScheme\",\n institution = \"Northeastern University College of Computer Science\",\n year = \t\"1992\",\n type = \t\"Technical Report\",\n number = \t\"NU-CCS-92-5\",\n OPTaddress = \t\"\",\n month = \tfeb,\n OPTnote = \t\"\",\n abstract = \"This document gives a summary of activities under\n\t\t MITRE Contract Number F19628-89-C-001. It gives a\n\t\t detailed denotational specification of the language\n\t\t Pure Pre\\-Scheme. A bytecode compiler, derived from\n\t\t the semantics, is presented, followed by proofs of\n\t\t correctness of the compiler with respect to the\n\t\t semantics. Finally, an assembler from the bytecode\n\t\t to an actual machine architecture is shown.\"\n}\n\n","author_short":["Oliva, D. P.","Wand, M."],"key":"OlivaWand92","id":"OlivaWand92","bibbaseid":"oliva-wand-averifiedcompilerforpureprescheme-1992","role":"author","urls":{},"downloads":0,"html":""},"search_terms":["verified","compiler","pure","prescheme","oliva","wand"],"keywords":[],"authorIDs":[],"dataSources":["zM8mNPR4ZkAHKtvDs"]}