SHF: Small: Foundations and Applications of Higher-Dimensional Directed Type Theory

SHF：小：高维定向类型理论的基础和应用

• 批准号: 1116703
• 负责人: Robert Harper
• 金额: $ 50万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2011
• 资助国家: 美国
• 起止时间: 2011-08-01 至 2015-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1116703&HistoricalAwards=false
• 关键词: SHF; Small; Foundations; Applications; Higher

A central objective for computer science is to develop methods for buildingreliable and maintainable software. The most important technique for ensuringthese properties is abstraction, the decomposition of a system into separableand reusable components. The theory of abstraction in programming is calledtype theory. A type is a specification of the behavior of a software component;type checking ensures that programs obey these specifications. This ensuresthat components can be modified or replaced without fear of disrupting thebehavior of other components. By supporting the expression and enforcement ofcomponent behaviors, type theory integrates programming with verification, theprocess of ensuring compliance with specifications. All modern programminglanguages and development methodologies are based on, or draw inspiration from,type theory. The broad goal of this project is to extend the capabilities oftype theory to a wider range of properties, and to use type theory to facilitatethe development of reliable software.Specifically, the research will develop the theory of higher-dimensional typetheory, and explore its application to generic programming, a techniquefor generating programs from their specifications. Higher-dimensionaltype theory draws on recent advances in category theory and algebraictopology that emphasize the algebraic structure of relations betweenprograms, and relations between such relations, in direct analogy withthe higher-dimensional structure of topological spaces. In this settingdependent families of types must respect the algebraic structure of suchrelations, and in doing so, they implicitly provide transformations thatcorrespond to generic programs whose behavior is determined by theirtype. More broadly, the project will apply ideas from category theoryand topology to improve software development, and apply ideas from typetheory to facilitate computer-verified proofs of mathematical theorems.

计算机科学的一个中心目标是开发构建可靠且可维护的软件的方法。 确保这些属性的最重要技术是抽象，即将系统分解为可分离和可重用的组件。 编程中的抽象理论称为类型理论。 类型是软件组件行为的规范；类型检查确保程序遵守这些规范。 这确保了可以修改或替换组件，而不必担心破坏其他组件的行为。 通过支持组件行为的表达和执行，类型理论将编程与验证（确保符合规范的过程）集成在一起。 所有现代编程语言和开发方法都基于类型理论或从中汲取灵感。 该项目的总体目标是将类型理论的功能扩展到更广泛的属性，并使用类型理论促进可靠软件的开发。具体来说，该研究将发展高维类型理论，并探索其在泛型编程中的应用，泛型编程是一种根据规范生成程序的技术。 高维类型理论借鉴了范畴论和代数拓扑学的最新进展，强调程序之间关系的代数结构以及这些关系之间的关系，与拓扑空间的高维结构直接类比。 在这种情况下，类型的依赖族必须尊重此类关系的代数结构，并且在这样做时，它们隐式地提供了与行为由其类型决定的通用程序相对应的转换。 更广泛地说，该项目将应用范畴论和拓扑学的思想来改进软件开发，并应用类型论的思想来促进数学定理的计算机验证证明。