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

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

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.