Mitchell Wand and Galen~B. Williamson. A Modular, Extensible Proof Method for Small-step Flow Analyses. In Daniel~Le M{\'e}tayer, editor, Programming Languages and Systems, 11th European Symposium on Programming, ESOP 2002, held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings, volume 2305 of Lecture Notes in Computer Science, pages 213--227, Berlin, Heidelberg, and New York, 2002. Springer-Verlag.
Abstract: We introduce a new proof technique for showing the correctness of 0CFA-like analyses with respect to small-step semantics. We illustrate the technique by proving the correctness of 0CFA for the pure lambda-calculus under arbitrary beta-reduction. This result was claimed by Palsberg in 1995; unfortunately, his proof was flawed. We provide a correct proof of this result, using a simpler and more general proof method. We illustrate the extensibility of the new method by showing the correctness of an analysis for the Abadi-Cardelli object calculus under small-step semantics.
Mitchell Wand. Analyses that Distinguish Different Evaluation Orders, or, Unsoundness Results in Control-Flow Analysis. unpublished note, July 2002.
Abstract: The standard control-flow analysis for higher-order languages, 0CFA, as defined by Sestoft, Shivers, Palsberg, et al., has been shown correct for a variety of semantics. One view of this family of results is that it shows that 0CFA is insensitive to evaluation order. We present simple modifications of 0CFA for call-by-value and call-by-name that distinguish call-by-value, call-by-name, and unrestricted beta-reduction.
Jens Palsberg and Mitchell Wand. CPS Transformation of Flow Information. Journal of Functional Programming, 13(5):905--923, September 2003.
Abstract: We consider the question of how a continuation-passing-style (CPS) transformation changes the flow analysis of a program. We present an algorithm that takes the least solution to the flow constraints of a program and constructs in linear time the least solution to the flow constraints for the CPS-transformed program. Previous studies of this question used CPS transformations that had the effect of duplicating code, or of introducing flow sensitivity into the analysis. Our algorithm has the property that for a program point in the original program and the corresponding program point in the CPS-transformed program, the flow information is the same. By carefully avoiding both duplicated code and flow-sensitive analysis, we find that the most accurate analysis of the CPS-transformed program is neither better nor worse than the most accurate analysis of the original. Thus a compiler that needed flow information after CPS transformation could use the flow information from the original program to annotate some program points, and it could use our algorithm to find the the rest of the flow information quickly, rather than having to analyze the CPS-transformed program.
Mitchell Wand and William D. Clinger. Set Constraints for Destructive Array Update Optimization. Journal of Functional Programming, 11(3):319--346, May 2001.
Abstract: Destructive array update optimization is critical for writing scientific codes in functional languages. We present set constraints for an interprocedural update optimization that runs in polynomial time. This is a multi-pass optimization, involving interprocedural flow analyses for aliasing and liveness. We characterize and prove the soundness of these analyses using small-step operational semantics. We also prove that any sound liveness analysis induces a correct program transformation.
A preliminary version of this paper appeared in ICCL '98.
Philippe Meunier, Robby Findler, Paul A. Steckler, and Mitchell Wand. Selectors Make Analyzing Case-Lambda Too Hard. In Proc. Scheme 2001 Workshop, Technical Report: Informatique, Signaux et Systemes de Sophia-Antipolis, I3S/RT-2001-12-FR, pages 54--64, September 2001.
Abstract: Flanagan's set-based analysis (SBA) uses selectors to choose data flowing through expressions. For example, the rng selector chooses the ranges of procedures flowing through an expression. The MrSpidey static debugger for PLT Scheme is based on Flanagan's formalism. In PLT Scheme, a case-lambda is a procedure with possibly several argument lists and clauses. When a case-lambda is applied at a particular call site, at most one clause is actually invoked, chosen by the number of actual arguments. Therefore, an analysis should propagate data only through appropriate case-lambda clauses. MrSpidey propagates data through all clauses of a case-lambda, lessening its usefulness as a static debugger. Wishing to retain Flanagan's framework, we extended it to better analyze case-lambda with rest parameters by annotating selectors with arity information. The resulting analysis gives strictly better results than MrSpidey. Unfortunately, the improved analysis is too expensive because of overheads imposed by the use of selectors. Nonetheless, a closure-analysis style SBA (CA-SBA) eliminates these overheads and can give comparable results within cubic time.
Mitchell Wand and Igor Siveroni. Constraint Systems for Useless Variable Elimination. In Proceedings 26th ACM Symposium on Programming Languages, pages 291--302, 1999.
Abstract: A useless variable is one whose value contributes nothing to the final outcome of a computation. Such variables are unlikely to occur in human-produced code, but may be introduced by various program transformations. We would like to eliminate useless parameters from procedures and eliminate the corresponding actual parameters from their call sites. This transformation is the extension to higher-order programming of a variety of dead-code elimination optimizations that are important in compilers for first-order imperative languages. Shivers has presented such a transformation. We reformulate the transformation and prove its correctness. We believe that this correctness proof can be a model for proofs of other analysis-based transformations.
Mitchell Wand and Gregory T. Sullivan. Denotational Semantics Using an Operationally-Based Term Model. In Proceedings 23rd ACM Symposium on Programming Languages, pages 386--399, 1997.
Abstract: We introduce a method for proving the correctness of transformations of programs in languages like Scheme and ML. The method consists of giving the programs a denotational semantics in an operationally-based term model in which interaction is the basic observable, and showing that the transformation is meaning-preserving. This allows us to consider correctness for programs that interact with their environment without terminating, and also for transformations that change the internal store behavior of the program. We illustrate the technique on some of the Meyer-Sieber examples, and we use it to prove the correctness of assignment elimination for Scheme. The latter is an important but subtle step for Scheme compilers; we believe ours is the first proof of its correctness.
Paul A. Steckler and Mitchell Wand. Lightweight Closure Conversion. ACM Transactions on Programming Languages and Systems, pages 48--86, January 1997. Original version appeared in Proceedings 21st ACM Symposium on Programming Languages, 1994.
Abstract: We consider the problem of lightweight closure conversion, in which multiple procedure call protocols may coexist in the same code. A lightweight closure omits bindings for some of the free variables of the procedure that it represents. Flow analysis is used to match the protocol expected by each procedure and the protocol used at each of its possible call sites. We formulate the flow nalysis as a deductive system tht generates a labelled transtiion system and a set of constraints. We show that any solution to the constraints justifies the rsulting transformation. Some of the techniques used a similar to those of abstract interpretation, but others appear to be novel.
Jerzy Tiuryn and Mitchell Wand. Untyped Lambda-Calculus with Input-Output. In H. Kirchner, editor, Trees in Algebra and Programming: CAAP'96, Proc. 21st International Colloquium, volume 1059 of Lecture Notes in Computer Science, pages 317--329, Berlin, Heidelberg, and New York, April 1996. Springer-Verlag.
Abstract: We introduce an untyped lambda-calculus with input-output, based on Gordon's continuation-passing model of input-output. This calculus is intended to allow the classification of possibly infinite input-output behaviors, such as those required for servers or distributed systems. We define two terms to be operationally approximate iff they have similar behaviors in any context. We then define a notion of applicative approximation and show that it coincides with operational approximation for these new behaviors. Last, we consider the theory of pure lambda-terms under this notion of operational equivalence.
Gregory T. Sullivan and Mitchell Wand. Incremental Lambda Lifting: An Exercise in Almost-Denotational Semantics. manuscript, November 1996.
Abstract: We prove the correctness of incremental lambda-lifting, an optimization that attempts to reduce the closure allocation overhead of higher-order programs by changing the scope of nested procedures. This optimization is invalid in the standard denotational semantics of Scheme, because it changes the storage behavior of the program. Our method consists of giving Scheme a denotational semantics in an operationally-based term model in which interaction is the basic observable. Lambda lifting is then shown to preserve meaning in the model.
Mitchell Wand and Zheng-Yu Wang. Conditional Lambda-Theories and the Verification of Static Properties of Programs. Information and Computation, 113(2):253--277, 1994. Preliminary version appeared in {\lics{5th}}, 1990, pp. 321-332.
Abstract: We present a proof that a simple compiler correctly uses the static properties in its symbol table. We do this by regarding the target code produced by the compiler as a syntactic variant of a \l-term. In general, this \l-term $C$ may not be equal to the semantics $S$ of the source program: they need be equal only when information in the symbol table is valid. We formulate this relation as a {\it {conditional \l-judgement}\/} $\Gbar \imp S = C$, where \Gbar\ is a formula that represents the invariants implicit in symbol table \G. We present rules of inference for conditional \l-judgements and prove their soundness. We then use these rules to prove the correctness of a simple compiler that relies on a symbol table. The form of the proof suggests that such proofs may be largely mechanizable.
Mitchell Wand. Specifying the Correctness of Binding-Time Analysis. Journal of Functional Programming, 3(3):365--387, July 1993. preliminary version appeared in {\it Conf. Rec. 20th ACM Symp. on Principles of Prog. Lang.\/} (1993), 137--143.
Abstract: Mogensen has exhibited a very compact partial evaluator for the pure lambda calculus, using binding-time analysis followed by specialization. We give a correctness criterion for this partial evaluator and prove its correctness relative to this specification. We show that the conventional properties of partial evaluators, such as the Futamura projections, are consequences of this specification. By considering both a flow analysis and the transformation it justifies together, this proof suggests a framework for incorporating flow analyses into verified compilers.
Mitchell Wand