@TechReport{WandSullivan95,
  author = 	"Mitchell Wand and Gregory T. Sullivan",
  title = 	"A Little Goes a Long Way: A Simple Tool to Support
  Denotational Compiler-Correctness Proofs",
  year = 	"1995",
  month =       nov,
  institution = "Northeastern University College of Computer Science",
  number = "NU-CCS-95-19",
  source = {~wand/unif/lfp/abstract.tex},
  URL =  {ftp://ftp.ccs.neu.edu/pub/people/wand/papers/wand-sullivan-95.ps},
  abstract =    "In a series of papers in the early 80's we proposed a
		 paradigm for semantics-based compiler correctness.
		 In this paradigm, the source and target languages are
		 given denotational semantics in the same
		 lambda-theory, so correctness proofs can be carried
		 out within this theory.  In many cases, the proofs
		 have a highly structured form.  We show how a simple
		 proof strategy, based on an algorithm for
		 alpha-matching, can be used to build a tool that can
		 automate all the routine cases of these proofs." 
}

{"_id":"4roXMmdPxi2WAntdp","bibbaseid":"wand-sullivan-alittlegoesalongwayasimpletooltosupportdenotationalcompilercorrectnessproofs-1995","downloads":0,"creationDate":"2017-04-23T20:31:12.578Z","title":"A Little Goes a Long Way: A Simple Tool to Support Denotational Compiler-Correctness Proofs","author_short":["Wand, M.","Sullivan, G. T."],"year":1995,"bibtype":"techreport","biburl":"http://www.ccs.neu.edu/home/wand/Bibliography.bib","bibdata":{"bibtype":"techreport","type":"techreport","author":[{"firstnames":["Mitchell"],"propositions":[],"lastnames":["Wand"],"suffixes":[]},{"firstnames":["Gregory","T."],"propositions":[],"lastnames":["Sullivan"],"suffixes":[]}],"title":"A Little Goes a Long Way: A Simple Tool to Support Denotational Compiler-Correctness Proofs","year":"1995","month":"November","institution":"Northeastern University College of Computer Science","number":"NU-CCS-95-19","source":"~wand/unif/lfp/abstract.tex","url":"ftp://ftp.ccs.neu.edu/pub/people/wand/papers/wand-sullivan-95.ps","abstract":"In a series of papers in the early 80's we proposed a paradigm for semantics-based compiler correctness. In this paradigm, the source and target languages are given denotational semantics in the same lambda-theory, so correctness proofs can be carried out within this theory. In many cases, the proofs have a highly structured form. We show how a simple proof strategy, based on an algorithm for alpha-matching, can be used to build a tool that can automate all the routine cases of these proofs.","bibtex":"@TechReport{WandSullivan95,\n author = \t\"Mitchell Wand and Gregory T. Sullivan\",\n title = \t\"A Little Goes a Long Way: A Simple Tool to Support\n Denotational Compiler-Correctness Proofs\",\n year = \t\"1995\",\n month = nov,\n institution = \"Northeastern University College of Computer Science\",\n number = \"NU-CCS-95-19\",\n source = {~wand/unif/lfp/abstract.tex},\n URL = {ftp://ftp.ccs.neu.edu/pub/people/wand/papers/wand-sullivan-95.ps},\n abstract = \"In a series of papers in the early 80's we proposed a\n\t\t paradigm for semantics-based compiler correctness.\n\t\t In this paradigm, the source and target languages are\n\t\t given denotational semantics in the same\n\t\t lambda-theory, so correctness proofs can be carried\n\t\t out within this theory. In many cases, the proofs\n\t\t have a highly structured form. We show how a simple\n\t\t proof strategy, based on an algorithm for\n\t\t alpha-matching, can be used to build a tool that can\n\t\t automate all the routine cases of these proofs.\" \n}\n\n","author_short":["Wand, M.","Sullivan, G. T."],"key":"WandSullivan95","id":"WandSullivan95","bibbaseid":"wand-sullivan-alittlegoesalongwayasimpletooltosupportdenotationalcompilercorrectnessproofs-1995","role":"author","urls":{"Paper":"ftp://ftp.ccs.neu.edu/pub/people/wand/papers/wand-sullivan-95.ps"},"downloads":0,"html":""},"search_terms":["little","goes","long","way","simple","tool","support","denotational","compiler","correctness","proofs","wand","sullivan"],"keywords":[],"authorIDs":[],"dataSources":["zM8mNPR4ZkAHKtvDs"]}