A Little Goes a Long Way: A Simple Tool to Support Denotational Compiler-Correctness Proofs

In a series of papers in the early 80's we proposed a paradigm for semanticsbased compiler correctness. In this paradigm, the source and target languages are given denotational semantics in the same -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 ff-matching, can be used to build a tool that can automate the routine cases of these proofs. 1 Introduction In a series of papers in the early 80's [19, 18, 20, 5] we proposed a paradigm for semantics-based compiler correctness, and over the last several years we have begun putting this paradigm into practice [22, 14]. In this paradigm, the source and target languages are given denotational semantics in the same -theory [11], so that most of the steps of the correctness proof can be done Work supported by the National Science Foundation under grant numbers CCR9014603 and CCR-9304144. within the t..