Technical Report NU-CCS-95-19, Northeastern University College of Computer Science, November, 1995.

Paper abstract bibtex

Paper abstract bibtex

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.

@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." }

Downloads: 0