Formal Methods for Object-Based Computing

对象是对封装可变内部状态并提供操作来操作状态的抽象进行编程。基于对象的计算是一种编程范例，它使用对象来组织程序中执行的状态操作。这个项目的目标是开发用于指定、概念化和推理基于对象的程序的形式化方法。这些形式化方法包括：(1)类型系统：基于对象的程序涉及哪些类型的语义实体，以及如何在程序设计语言的类型系统中捕获它们？(2)指称语义：捕获基于对象的程序的行为涉及哪些数学抽象？(3)规范：如何指定单个对象的行为？(4)推理方法：什么方法适合于证明基于对象的程序的性质？正在追求的方向是在函数式编程几十年的研究基础上再接再厉，以便在使用基于对象的程序时实现编程概念和数学工具的“紧密集成”。主要关注的是使用基于lambda演算的高阶语言框架的代数规范和等式推理技术。***

Objects are programming abstractions that encapsulate mutable internal state and provide operations to manipulate the state. Object-based computing is the programming paradigm that uses objects to structure the state-manipulation carried out in programs. The goal of this project is to develop formal methods for specifying, conceptualizing, and reasoning about object- based programs. These formal methods include: (1) Type systems: what kinds of semantic entities are involved in object-based programs, and how does one capture them in type systems for programming languages? (2) Denotational semantics: what mathematical abstractions are involved in capturing the bahaviors of object-based programs? (3) Specifications: How does one specify the behaviors of individual objects? (4) Reasoning methods: what methods are appropriate and useful for proving properties of object-based programs? The Direction being pursued is to build on the several decades of research in functional programming so as ato achieve a "tight integration" of programming concepts and mathmatical tools in working with object-based programs. Of primary focus are algebraic specification and equational reasoning techniques using lambda-calculus-based higher-order language frameworks. ***