Research

## Type Theory

- Dependent Types
- Homotopy Type Theory

## Functional Programming

- Algebra of Programming
- Connections with Machine Learning

## Applications

- Proof Evolution, with Talia Ringer, Nate Yazdani and Dan Grossman at the University of Washington
- Core Agda Specification with Andreas Abel, Jesper Cockx and Youyou Cong
- Adding dependent types to Haskell
- Music: Analysis and Synthesis
- Education, in particular tools for teachers
- Formal mathematical proof
- Natural Language (e.g., Grammatical Framework)