Systems of Variable Type

9302923 Feferman现代编程语言可以操纵潜在的无限对象（流，任意精度实数等）。示例包括：Haskell、ML和其他函数式语言、Ada（例如任务和过程）和c++（对象本质上是高阶实体）。实时应用程序具有涉及模拟/连续和离散实体以及这些领域之间关系的规范。要为这类应用程序开发函数式编程语言的形式化方法，并为大规模编程强制规范和程序的模块化构造，需要比大多数文献中所处理的更一般（非代数）的抽象数据类型（adt）概念。然后必须解决几个问题，包括以下问题：如何丰富ADT的概念（广义ADT）以包含这些对象？用这些对象进行计算意味着什么？重要的是要有一种超越有限表示操作的理解。通过声明这样的adt来丰富逻辑理论的合适的形式符号是什么？本研究将集中于以下三个密切相关的主题：广义ADT的计算，广义ADT的定义系统，以及在广义ADT设置下制定的大量验证示例。该项目将继续在可变类型（VT）理论的框架内开展工作。＊＊＊

9302923 Feferman Modern programming languages manipulate potentially infinite objects (streams, arbitrary precision reals, etc.). Examples include: Haskell, ML, and other functional languages, Ada (for example tasks and processes), and C++ (objects being essentially higher-order entities). Real-time applications have specifications that involve both analog/continuous and discrete entities and relations between these domains. To develop formal methods for functional programming languages for such applications, and to enforce modular construction of specifications and programs for programming-in-the-large, one needs more general (non-algebraic) notions of abstract data types (ADTs) than have been treated in most of the literature. Several questions must then be addressed, including the following: How can the notion of ADT be enriched (generalized ADTs) to encompass such objects? What does it mean to compute with these objects? It is important to have an understanding beyond just manipulation of finite representations. What is a suitable formal notation for enriching logical theories by declaring such ADTs? This research would focus on the following three closely related topics: computation over generalized ADTs, systems for definition of generalized ADTs, and substantial verification examples worked out within the generalized ADT setting. The project will continue work within the framework of variable type (VT) theories. ***