Dependent type theories are a family of programming languages distinguished by their rich and expressive static type systems. There is a close link between the design and analysis of type theories and category theory (an area of abstract mathematics). By exploiting this relationship, we are able to reason about existing type theories as well as a mechanism for designing extensions to these systems better suited for novel applications. 

This research enhances the reliability and security of critical software systems by enabling the design of safer, more expressive programming languages.