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