Canonicity for Two-Dimensional Type Theory – Københavns Universitet

Canonicity for Two-Dimensional Type Theory

COPLAS Talk by Robert Harper, Carnegie-Mellon University


Higher-dimensional dependent type theory enriches conventional one-dimensional dependent type theory with additional structure expressing equivalence of elements of a type. This structure may be employed in a variety of ways to capture rather coarse identifications of elements, such as a universe of sets considered modulo isomorphism. Equivalence must be respected by all families of types and terms, as witnessed computationally by a type-generic program. Higher-dimensional type theory has applications to code reuse for dependently typed programming, and to the formalization of mathematics. In this paper, we develop a novel judgemental formulation of a two-dimensional type theory, which enjoys a canonicity property: a closed term of boolean type is definitionally equal to true or false. Canonicity is a necessary condition for a computational interpretation of type theory as a programming language, and does not hold for existing axiomatic presentations of higher-dimensional type theory. The method of proof is a generalization of the NuPRL semantics, interpreting types as syntactic groupoids rather than equivalence relations.
This talk reports about joint work with Daniel R. Licata.

Robert Harper is a Professor of Computer Science at Carnegie Mellon University, where he has been a member of the faculty of the Computer Science Department since 1988. His main research interest is in the application of constructive type theory to the design and implementation of programming languages and to the development of systems for mechanization of mathematics. He is probably best known for his work on the design and implementation of Standard ML, for the introduction of the LF logical framework, and for the development of the concept of a type-directed certifying compiler based on typed intermediate languages.