Research

## Type Theory

- Dependent Types
- Homotopy Type Theory

## Functional Programming

- Algebra of Programming
- Connections with Machine Learning

## Applications

- Adding dependent types to Haskell
- Further improvements to Agda
- Music: Analysis and Synthesis
- Education, in particular tools for teachers
- Formal mathematical proof
- Natural Language (e.g., Grammatical Framework)