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.
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.
| College of Computer Science
| Northeastern University]