David Gladstein and Mitchell Wand. Compiler Correctness for Concurrent Languages. In Paolo Ciancarini and Chris Hankin, editors, Proc. Coordination '96 (Cesena, Italy), volume 1061 of Lecture Notes in Computer Science, pages 231--248, Berlin, Heidelberg, and New York, April 1996. Springer-Verlag.
Abstract: This paper extends previous work in compiler derivation and verification to languages with true-concurrency semantics. We extend the lambda-calculus to model process-centered concurrent computation, and give the semantics of a small language in terms of this calculus. We then define a target abstract machine whose states have denotations in the same calculus. We prove the correctness of a compiler for our language: the denotation of the compiled code is shown to be strongly bisimilar to the denotation of the source program, and the abstract machine running the compiled code is shown to be branching-bisimilar tothe source program's denotation.
Mitchell Wand. Compiler Correctness for Parallel Languages. In Functional Programming Languages and Computer Architecture, pages 120-134, June 1995.
Abstract: We present a paradigm for proving the correctness of compilers for languages with parallelism. The source language is given a denotational semantics as a compositional translation to a higher-order process calculus. The target language is also given a denotational semantics as a compositional translation to the same process calculus. We show the compiler is correct in that it preserves denotation up to bisimulation. The target language is also given an operational semantics, and this operational semantics is shown correct in the sense that it is branching-bisimilar to the denotational semantics of the target language. Together, these results show that for any program, the operational semantics of the target code is branching-bisimilar to the semantics of the source code.
Dino P. Oliva, John D. Ramsdell, and Mitchell Wand. The VLISP Verified PreScheme Compiler. Lisp and Symbolic Computation, 8(1/2):111-182, 1995.
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.
Joshua D. Guttman and Mitchell Wand, editors. VLISP: A Verified Implementation of Scheme. Kluwer, Boston, 1995. Originally published as a special double issue of the journal Lisp and Symbolic Computation (Volume 8, Issue 1/2).
Abstract: The VLISP project undertook to verify rigorously the implementation of a programming language. The project began at The MITRE Corporation in late 1989, under the company's Technology Program. The work was supervised by the Rome Laboratory of the United States Air Force. Northeatern University became involved a year later. This research work has also been published as a special double issue of the journal Lisp and Symbolic Computation (Volume 8, Issue 1/2).
Joshua Guttman, John Ramsdell, and Mitchell Wand. VLISP: A Verified Implementation of Scheme. Lisp and Symbolic Computation, 8(1/2):5-32, 1995.
Abstract: The Vlisp project showed how to produce a comprehensively verified implementation for a programming language, namely Scheme. This paper introduces two more detailed studies on Vlisp. It summarizes the basic techniques that were used repeatedly throughout the effort. It presents scientific conclusions about the applicability of the these techniques as well as engineering conclusions about the crucial choices that allowed the verification to succeed.
Mitchell Wand and Dino P. Oliva. Proving the Correctness of Storage Representations. In Lisp and Functional Programming 1992, pages 151-160, 1992.
Abstract: Conventional techniques for semantics-directed compiler de\-ri\-vation yield abstract machines that manipulate trees. However, in order to produce a real compiler, one has to represent these trees in memory. In this paper we show how the technique of {\em {storage-layout relations}} (introduced by Hannan \cite{Hannan}) can be applied to verify the correctness of storage representations in a very general way. This technique allows us to separate denotational from operational reasoning, so that each can be used when needed. As an example, we show the correctness of a stack implementation of a language including dynamic catch and throw. The representation uses static and dynamic links to thread the environment and continuation through the stack. We discuss other uses of these techniques.
Mitchell Wand. Correctness of Procedure Representations in Higher-Order Assembly Language. In S. Brookes, editor, Proceedings Mathematical Foundations of Programming Semantics '91, volume 598 of Lecture Notes in Computer Science, pages 294-311. Springer-Verlag, Berlin, Heidelberg, and New York, 1992.
Abstract: Higher-order assembly language (HOAL) generalizes combinator-based target languages by allowing free variables in terms to play the role of registers. We introduce a machine model for which HOAL is the assembly language, and prove the correctness of a compiler from a tiny language into HOAL. We introduce the notion of a lambda-representation, which is an abstract binding operation, show how some common representations of procedures and continuations can be expressed as lambda-representations. Last, we prove the correctness of a typical procedure-calling convention in this framework.
Dino P. Oliva and Mitchell Wand. A Verified Run-Time Structure for Pure PreScheme. Technical Report NU-CCS-92-97, Northeastern University College of Computer Science, 1992.
Abstract: This document gives a summary of activities under MITRE Corporation Contract Number F19628-89-C-0001. It gives an operational semantics of an abstract machine for Pure PreScheme and of its implementation as a run-time structure on an Motorola 68000 microprocessor. The relationship between these two models is stated formally and proved.
Dino P. Oliva and Mitchell Wand. A Verified Compiler for Pure PreScheme. Technical Report NU-CCS-92-5, Northeastern University College of Computer Science, February 1992.
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.
Mitchell Wand. A Short Proof of the Lexical Addressing Algorithm. Information Processing Letters, 35:1-5, 1990.
Abstract: The question of how to express binding relations, and in particular, of proving the correctness of lexical addressing techniques, has been considered primarily in the context of compiler correctness proofs. Here we consider the problem in isolation. We formulate the connections between three different treatments of variables in programming language semantics: the environment coding, the natural coding, and the lexical-address coding (sometimes called the Frege coding, the Church coding, and the deBruijn coding, respectively). By considering the problem in isolation, we obtain shorter and clearer proofs. The natural coding seems to occupy a central place, and the other codings are proved equivalent by reference to it.
Abstract: We present a new abstract machine model for compiling languages based on their denotational semantics. In this model, the output of the compiler is a lambda-term which is the higher-order abstract syntax for an assembly language program. The machine operates by reducing these terms. This approach is well-suited for generating code for modern machines with many registers. We discuss how this approach can be used to prove the correctness of compilers, and how it improves on our previous work in this area.
Mitchell Wand. From Interpreter to Compiler via Higher-Order Abstract Assembly Language. Technical report, Northeastern University College of Computer Science, 1989.
Abstract: In this paper, we give a case study of transforming an interpreter into a compiler. This transformation improves on our previous work through the use of higher-order abstract assembly language. Higher-order abstract assembly language (or HOAL) uses a Church-style, continuation-passing encoding of machine operations. This improves on the use of combinator-based encoding in allowing a direct treatment of register usage, and thereby giving the compiler writer a clearer idea of how to incorporate new constructs in the source language or machine. For example, it allows a denotational exposition of stack layouts. We show how to do the transformation for a simple language, for a language with procedures, and for a compiler using lexical addresses.
Mitchell Wand. From Interpreter to Compiler: A Representational Derivation. In H. Ganzinger and N.D. Jones, editors, Workshop on Programs as Data Objects, volume 217 of Lecture Notes in Computer Science, pages 306-324. Springer-Verlag, Berlin, Heidelberg, and New York, 1985.
Mitchell Wand. Embedding Type Structure in Semantics. POPL 1985, pages 1-6.
Abstract: We show how a programming language designer may embed the type structure of of a programming language in the more robust type structure of the typed lambda calculus. This is done by translating programs of the language into terms of the typed lambda calculus. Our translation, however, does not always yield a well-typed lambda term. Programs whose translations are not well-typed are considered meaningless, that is, ill-typed. We give a conditionally type-correct semantics for a simple language with continuation semantics. We provide a set of static type-checking rules for our source language, and prove that they are sound and complete: that is, a program passes the typing rules if and only if its translation is well-typed. This proves the correctness of our static semantics relative to the well-established typing rules of the typed lambda-calculus.
W. Clinger, D.P. Friedman, and Mitchell Wand. A Scheme for a Higher-Level Semantic Algebra. In J. Reynolds and M. Nivat, editors, Algebraic Methods in Semantics: Proceedings of the US-French Seminar on the Application of Algebra to Language Definition and Compilation, pages 237-250. Cambridge University Press, Cambridge, 1985.
Mitchell Wand. Loops in Combinator-Based Compilers. Information and Computation, 57(2-3):148-164, 1983. Previously appeared in POPL 1983, pages 190-196.
Abstract: In our paper [Wand 82a], we introduced a paradigm for compilation based on combinators. A program from a source language is translated (via a semantic definition) to trees of combinators; the tree is simplified via associative and distributive laws) to a linear, assembly-language-like format; the "compiler writer's virtual machine'' operates by simulating a reduction sequence of the simplified tree. The correctness of these transformations follows from general results about the $\lambda$-calculus. The code produced by such a generator is always tree-like. In this paper, the method is extended to produce target code with explicit loops. This is done by re-introducing variables into the terms of the target language in a restricted way, along with a structured binding operator. We also consider general conditions under which these transformations hold.
Mitchell Wand. Semantics-Directed Machine Architecture. POPL 1982, pages 234-241.
Mitchell Wand. Deriving Target Code as a Representation of Continuation Semantics. ACM Transactions on Programming Languages and Systems, 4(3):496-517, July 1982.
Last modified: Wed Jan 7 16:20:04 Eastern Standard Time 2015