My research is between computer architecture and programming languages. I work on leveraging high-level hardware programming languages to design hardware. I am especially interested in leveraging those hardware programming languages to ease verification, which is typically a significant part of the development effort. Especially, I often try to use theorem proving to state and prove the properties of different architectures. In the past, I worked on domain-specific hardware accelerators and I studied various unintended security consequences of modern microarchitectural features in our out-of-order processor (see our riscy-OOO project).