Very little work has been done on the nature of program equivalence for typed higher-order languages with imperative features. In this project, investigations will continue into reasoning about programs with side-effects and other imperative features such as control abstractions. In particular, the semantics of various typed lambda calculi with references or pointers will be investigated. Simple types will be studied initially and a variety of extensions including polymorphism, effect systems, and control abstractions will then be explored. One aim of the research is to develop calculi of constrained equivalence which take into consideration the fact that a program or expression will only be used in certain contexts. In addition, the problem of providing for object-oriented programming in typed languages will be studied. This includes specifying classes of objects and defining notions of equivalence for objects and specifications of classes. This work can be seen from two points of view. First as studying typed fragments of untyped languages, axiomatizing program equivalence relative to a set of typed contexts and developing formal mechanisms for embedding typed fragments in untyped languages. Second as adding reference types and other imperative features and studying the effect of these additions on various type systems and on the nature of program equivalence.
