Semantics of Computation

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

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.