Axiomatizing Program Equivalence in Typed Functional Languages with Imperative Features

具有命令式特征的类型化函数语言中的程序等价公理化

• 批准号: 8915663
• 负责人: John McCarthy
• 金额: $ 29.87万
• 依托单位: Stanford University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1990
• 资助国家: 美国
• 起止时间: 1990-07-15 至 1993-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=8915663&HistoricalAwards=false
• 关键词: Axiomatizing; Program; Equivalence; Typed; Functional

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.

关于程序的性质， 等价于具有命令式特征的类型化高阶语言。 在这个项目中，调查将继续推理， 具有副作用和其他强制性功能的程序，例如 控制抽象。 特别是，各种类型的 将研究具有引用或指针的lambda演算。 首先将研究简单类型， 包括多态性、效果系统和控制抽象， 然后被探索。 这项研究的目的之一是开发 约束等价，考虑到一个事实， 程序或表达式将仅在某些上下文中使用。 在 此外，在中提供面向对象编程的问题 将学习类型化语言。 这包括指定 对象和定义对象的等价概念， 类的规格。 这项工作可以从两个角度来看。 首先，学习 非类型化语言的类型化片段，公理化程序等价 相对于一组类型化上下文和开发正式机制 用于在非类型化语言中嵌入类型化片段。 第二，增加 指称类型和其他祈使特征，并研究其作用 这些补充对各种类型的系统和性质的 程序等价性