My research focuses on declarative programming systems for high-performance automated reasoning and the design and implementation of tunable correct-by-design analyses of complex systems and especially software: mainly of higher-order, functional and logical languages. I also work on compiling, parallelizing, and incrementalizing such analyses, and on their applications—software verification, optimization, and auditing. More broadly, my interests include semantics, language design, compilers and their implementation, safety and verification, parallelism and high-performance logic solvers. Contact me if you have an idea which intersects with my research or broader interests and want to discuss it. I am looking for students!