Relating Static and Dynamic Semantics of Programs

编程语言中的一个关键问题是设计和实现静态（编译时）和动态（运行时）计算阶段之间的平衡。 良好的平衡允许生成良好的代码，而不会给程序员或编译器带来不必要的负担。 找到这种平衡主要依赖于直觉和实验，但这些方法本身是不够的。 随着类型系统和优化转换变得越来越复杂，提供严格的方法来在适当的抽象级别上表达静态/动态关系变得至关重要。 程序员和编译器编写者依赖于这些关系，因此对它们进行精确但易于理解的描述非常重要。 仅仅使用直觉和实验可能会让错误或有价值的概括机会被忽视。 该项目的目标是开发和应用严格表达和证明编程语言的静态和动态语义之间的关系的技术。 主要目标包括：（i）找到在适合于共享、复制和活性推理的抽象层次上指定含义的方法;（ii）开发以正式方式表示和操作语义规范的方法;（三）通过制定描述模块兼容性保证系统的特性的技术，帮助开发新的接口定义语言，整合他们。

A key problem in programming languages is the design and implementation of a balance between static (compile-time) and dynamic (run-time) phases of computation. A good balance allows the generation of good code without an undue burden on programmers or compilers. Finding this balance relies critically on intuition and experimentation, but these methods are not enough by themselves. As type systems and optimizing transformations have become more sophisticated, it has become essential to provide rigorous means to express static/dynamic relationships at suitable levels of abstraction. Programmers and compiler writers rely on these relationships, so a precise but approachable description of them is important. Using intuition and experimentation alone may allow errors or valuable opportunities for generalization to go unnoticed. The goal of this project is to develop and apply techniques for rigorously expressing and proving the relationships between static and dynamic semantics of programming languages. Primary objectives include (i) finding ways to specify meanings at levels of abstraction suitable for reasoning about sharing, copying, and liveness; (ii) developing ways to represent and manipulate semantic specifications in a formal manner; (iii) aiding the development of new interface definition languages by formulating techniques for describing the properties that compatibility of modules guarantees for systems that integrate them.