Research Interests
- Verified Software Development and Dependently Typed Programming
- Type Theory, Functional Programming, Rewriting, and Termination
- Type Checking, Unification, and Compiling Dependent Types
- Linear and Modal Typing and Coeffects
- Constructive Logic and Logical Frameworks
- Theorem Proving and Program Verification