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.