Some research themes that make me tick, a quick and incomplete thread:
Conversation
In type theory, there's always a choice whether to make something internal or external. When we take something and make it internal to a type theory---like univalence---we usually learn a lot about it and refine it. I like to take those internal things and pull them back out.
2
6
Lots of type theorists like developing the type theory but then don't like building automation and tooling. I like to take the gunk the type theorists don't like to do and build awesome automation and tooling around beautiful type theory, like ornaments and transport.
2
11
Type theory is great and all, but I want real people to use it. What is painful about using new type theories? How can I make it less painful?
1
7
Proofs of program correctness are great, but they are too hard for mortals right now. How can I help mortals write and maintain proofs of program correctness?
1
11
What are the practical engineering implications of what's new and hot in type theory, like cubical? How can I build bridges between type theorists and the folks who work on more PLDI-type work?
1
8
Software engineers and proof engineers hate using new things. How can I take hot new concepts from programming languages and give it to engineers without making them ever switch languages and with minimal tooling overhead, in a way that naturally integrates with their workflows?
2
4
I'd like to know this too - super excited about coming up with new ways of describing this stuff to help them understand, but I'd also like there to be nice, easy to use IDE tooling for them to try out once they are intrigued as well.
1
1
And also integrating well with existing languages/ecosystems, through reliable build tooling and package management.