Systems of Variable Type

9302923费尔曼现代编程语言处理潜在的无限对象(流、任意精度的实数等)。例如：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. ***