Systems of Variable Type

9302923 Feferman现代编程语言操纵潜在的无限对象（流，任意精度实数等）。 示例包括：Haskell、ML和其他函数式语言、Ada（例如任务和进程）和C++（对象本质上是高阶实体）。 实时应用程序的规范涉及模拟/连续和离散实体以及这些域之间的关系。 为了开发用于此类应用的函数式编程语言的形式化方法，并为大型编程实施规范和程序的模块化构造，人们需要比大多数文献中处理的更一般（非代数）的抽象数据类型（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. ***