Axiomatizing Program Equivalence in Typed Functional Languages with Imperative Features

对于具有命令式特性的高阶类型化语言的程序等价的性质，研究得很少。在这个项目中，调查将继续对具有副作用和其他命令式特性（如控制抽象）的程序进行推理。特别地，将研究带有引用或指针的各种类型lambda演算的语义。我们将首先研究简单类型，然后探索包括多态性、效果系统和控制抽象在内的各种扩展。研究的目的之一是开发约束等价的演算，考虑到一个程序或表达式只会在某些情况下使用。此外，还将研究在类型语言中提供面向对象程序设计的问题。这包括指定对象的类，定义对象和类的规范的等价概念。这项工作可以从两个角度来看待。首先，研究非类型化语言的类型化片段，对一组类型化上下文的程序等价进行公理化，并开发在非类型化语言中嵌入类型化片段的形式化机制。第二，增加引用类型和其他命令式特性，并研究这些添加对各种类型系统和程序等价性质的影响。

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.