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.