Exploring New Constructs in Computational Type Theory

计算机科学越来越关注类型的概念。从60年代开始，这个概念已经证明了它作为一个有效的组织概念的价值——首先在编程和编程语言中，然后在知识表示、自动推理、形式化方法中，现在可能在计算机代数系统中。以前nsf支持的研究已经导致了一个连贯的建设性类型理论家族，并在康奈尔大学和其他相关系统的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.