I am broadly interested in compilers and tools related to compilers, such as in producing tools to enable new kinds of programming, including tools built on proof assistants and SMT solvers to develop programs with proven correctness properties and compilers for domain-specific languages that better encode expert knowledge to achieve greater performance and expressiveness.