Exploring New Constructs in Computational Type Theory

计算机科学越来越关注类型的概念。从60年代起，S就证明了这个概念作为一种有效的组织概念的价值--最初在程序设计和程序设计语言中，然后在知识表示、自动推理、形式方法中，现在可能在计算机代数系统中。以前由国家科学基金会支持的研究已经导致了一系列连贯的建构型理论，并在康奈尔大学的Nuprl系统和其他地方的相关系统中实施了这些理论。调查的计划是找到正确的概念来解释计算机代数系统中类型的使用以及抽象计算数学(特别是代数)的形式化。有人推测，在某些情况下，正确的概念是代数数据类型到高阶ADT的推广。在其他情况下，可能需要新的类型构造函数，例如非常依赖的类型。预计这些概念将澄清实用问题和基本问题。此外，研究方法试图将代数系统的面向对象特征形式化，并将其推广到其他编程环境。这项研究的结果使新一代计算机系统的设计成为可能，该系统围绕用于指定和验证链接协议的丰富类型概念集成了子系统(如编译器、具体和符号求值器、转换系统、证明器和数据库管理器)。对计算类型理论的研究也加深了对计算机科学的基础及其与数学和计算科学的联系的理解。

Computer science has become increasingly concerned with the concept of type. From the 60's onward this notion has demonstrated its value as an effective organizing concept_first in programming and programming languages, then in knowledge representation, in automated reasoning, in formal methods, and now perhaps in computer algebra systems. Previous NSF-supported research has led to a coherent family of constructive type theories and to the implementation of them in the Nuprl system from Cornell and related systems elsewhere. The plan of the investigation is to find the right concepts to explain the use of types in computer algebra systems and in formalizations of abstract computational mathematics (especially algebra). It is conjectured that in some cases the right concepts are generalizations of algebraic data types to higher-order ADT's. In other cases, new type constructors may be necessary, such as the very dependent types. These concepts are expected to clarify both pragmatic issues and foundational questions. Moreover, the method of investigation seeks to formalize the object oriented features of algebra systems and generalize them to other programming environments. The result of this research enables the design of a new generation of computer system that integrates subsystems (such as compilers, concrete and symbolic evaluators, transformation systems, provers, and data base managers) around a rich notion of type used to specify and verify the linking protocols. Investigation of computational type theory also deepens understanding of the foundations of computer science and its links to mathematics and computational science.