CV · GitHub · Google Scholar · ORCID · LinkedIn

Hello! My name is Kesha. I’m a computer science researcher at Sandia National Laboratories, and I’m interested in compilers, program analysis, and formal verification.

I earned my PhD in 2022 in Computer Science at the University of Maryland, where I was advised by Michael Hicks, and my undergraduate degree in Computer Science at the University of Minnesota.

For my dissertation, I designed and implemented SQIR, a small quantum intermediate representation embedded in the Rocq proof assistant, and VOQC, a verified optimizer for quantum circuits. You can read more about both in this blog post or in my dissertation.

From 2022 to 2024, I was an Applied Scientist in the Automated Reasoning in Identity group at Amazon Web Services (AWS), where I worked on the Cedar authorization language.

Selected publications

The full list is on my CV and on Google Scholar.

• How We Built Cedar: A Verification-Guided Approach. Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, John Kastner, Anwar Mamat, Matt McCutchen, Neha Rungta, Bhakti Shah, Emina Torlak, Andrew Wells. FSE, 2024. paper · DOI · code
• A Formally Certified End-to-end Implementation of Shor’s Factorization Algorithm. Yuxiang Peng, Kesha Hietala, Runzhou Tao, Liyi Li, Robert Rand, Michael Hicks, Xiaodi Wu. PNAS, 2023. paper · DOI
• Proving Quantum Programs Correct. Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks. ITP, 2021. paper · DOI · code
• A Verified Optimizer for Quantum Circuits. Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks. POPL, 2021. paper · DOI · code. Distinguished paper.