Publications

In this paper we give several examples that illustrate our techniques for reasoning about programs with effects. One technique is to define correspondences between effect-free programs and programs with effect and transfer results about effect-free programs to corresponding programs with effects. We give two examples of this technique. The first involves the correspondence between loops and tail-recursive programs, replacing assignment to loop variables by \qlet binding. The second example involves a correspondence between mutable objects and streams, replacing updating by explicitly passing the store. The correspondences are left informal here, but in practice translators can be defined to insure correct correspondences (and avoid the work of hand translation). A second technique is to lift principles for reasoning about effect-free programs to those with effects, typically by finding appropriate abstractions and restrictions. We present three examples here: the use of structure copying to insure non-interference among operations; the use of structural induction principles for establishing program equivalence; and the use of abstract objects to encapsulate effects and potential interference in a controlled way.