Semantics of Computation

这个项目将继续研究计算的语义。下一阶段的重点将放在证明编译器正确性的方法上。使用高阶汇编语言而不是组合子作为编译器目标代码的模型，使得编译器抽象机器的体系结构具有很大的灵活性；这种灵活性将用于证明各种不同环境和代码表示的正确性。第二个线程是面向对象系统强类型工作的延续；这里将研究有关子类型和强制的各种问题。

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.