Effect-dependent Program Equivalences for Objects
From PUMA Graduiertenkolleg
In a running project [benton06,benton0] in cooperation with Benton and Kennedy from Microsoft Research, we (Hofmann and Beringer) use information obtained through effect analysis to justify effect-depending program transformations such as code motion or code hoisting in a semantically clean way. One important tool to obtain these results is a "relational semantics of side effects" which we have developed earlier.
Starting-point of the proposed research is the design of an expressive effect system for Java with inheritance. We believe that a suitable modification and extension of the type system for objects [HofmannJ06] would do the job. Depending to interest, one could try to further develop the automatic type inference, e.g., by relying on techniques from static analysis and/or model-checking, or to explore the relational semantics of such a system together with the thus provable program transformations.