This project will continue research on the semantics of computation. The emphasis during the coming period will be on methods for proving the correctness of compilers. The use of higher-order assembly language rather than combinators as a model of a compiler's target code allows great flexibility in the architecture of the compiler's abstract machine; this flexibility will be used to prove the correctness of a variety of different environment and code representations. A second thread is a continuation of work on strong typing for object-oriented systems; here a variety of issues concerning subtyping and coercion will be studied.
