Home

Education

• PhD in Computer Science, University of Maryland, 2022
  • Dissertation: A Verified Software Toolchain for Quantum Programming
  • Advised by Michael Hicks
• MS in Computer Science, University of Maryland, 2019
• BS in Computer Science, summa cum laude, University of Minnesota, 2016
  • Minors in Mathematics and Asian Languages and Literatures (Japanese)

Work experience

• Computer Science Researcher, Sandia National Laboratories, 2024 – present
• Applied Scientist, Amazon Web Services (AWS), 2022 – 2024

As a student, I held several internships:

• Microsoft Quantum, Summer 2021
• Microsoft Research, Winter 2020
• Institute for Defense Analyses, Center for Computing Sciences, Summer 2017
• National Security Agency, Summers 2015 & 2016
• MIT Lincoln Laboratory, Summer 2014
• Sandia National Laboratories, Summers 2012 & 2013

Publications

• 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
• Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization. Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Lef Ioannidis, John Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, Andrew Wells. OOPSLA, 2024. paper · DOI · code
• A Verified Optimizer for Quantum Circuits (Journal Version). Kesha Hietala, Robert Rand, Liyi Li, Shih-Han Hung, Xiaodi Wu, Michael Hicks. TOPLAS, 2023. 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
• FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores. Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy. CPP, 2023. paper · DOI
• Verified Compilation of Quantum Oracles. Liyi Li, Finn Voichick, Kesha Hietala, Yuxiang Peng, Xiaodi Wu, Michael Hicks. OOPSLA, 2022. paper · DOI · code
• Q# as a Quantum Algorithmic Language. Kartik Singhal, Kesha Hietala, Sarah Marshall, Robert Rand. QPL, 2022. paper
• 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.
• Finding Substitutable Binary Code By Synthesizing Adapters. Vaibhav Sharma, Kesha Hietala, Stephen McCamant. IEEE TSE, 2019. DOI
• Formal Verification vs. Quantum Uncertainty. Robert Rand, Kesha Hietala, Michael Hicks. SNAPL, 2019. paper
• Quantitative Robustness Analysis of Quantum Programs. Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, Xiaodi Wu. POPL, 2019. paper · DOI
• Volume-Based Merge Heuristics for Disjunctive Numeric Domains. Andrew Ruef, Kesha Hietala, Arlen Cox. SAS, 2018. DOI
• Finding Substitutable Binary Code for Reverse Engineering by Synthesizing Adapters. Vaibhav Sharma, Kesha Hietala, Stephen McCamant. ICST, 2018. DOI

Drafts

• Q★: Implementing Quantum Separation Logic in F★
  Kesha Hietala, Sarah Marshall, Robert Rand, Nikhil Swamy
  Extended abstract presented by Robert Rand at PLanQC 2022 (slides). This project is no longer active.
• Quantum Programming Languages
  Kesha Hietala
  Course project write-up, December 2016. Written for readers with a basic understanding of quantum computation and no background in programming languages.
• Detecting Behaviorally-Equivalent Functions via Symbolic Execution
  Kesha Hietala
  Undergraduate thesis, May 2016. Supervised by Stephen McCamant.

Talks

• Verification-Guided Development of the Cedar Authorization Language. Presentation, HCSS 2023, Annapolis, MD, May 2023. slides
• A Verified Software Toolchain for Quantum Programming. Dissertation defense, University of Maryland, College Park, MD, May 2022. slides
• Quantum IRs for Formal Verification. Invited talk, QCE21 Workshop on Quantum Intermediate Representations, Virtual, October 2021. slides
• Proving Quantum Programs Correct. Paper presentation, ITP 2021, Virtual, June 2021. slides
• Expanding the VOQC Toolkit. Extended abstract, PLanQC 2021, Virtual, June 2021. slides · video
• A Verified Optimizer for Quantum Circuits. Paper presentation, POPL 2021, Virtual, January 2021. slides · video
• Approaches to Compiling Functional Languages. Two-part lecture given to a seminar on functional programming, University of Minnesota, Minneapolis, MN, May 2016. slides

Posters

• Verified Optimization in a Quantum Intermediate Representation
  Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks
  Presented at the Workshop on Noisy Intermediate-Scale Quantum Technologies (NISQ) 2019.
• Finding Semantically Equivalent Binary Code By Synthesizing Adaptors
  Kesha Hietala, Vaibhav Sharma, Stephen McCamant
  Presented at the 2017 Grad Cohort Workshop.
• A Comparison of Approaches to Compiling Functional Programming Languages
  Kesha Hietala
  Presented at the University of Minnesota Undergraduate Research Symposium and Winchell Undergraduate Research Symposium, May 2015.

Teaching and mentorship

• Project lead for the Tech+Research track at Technica, 2019 & 2022 (code)
• Volunteer for the quantum track of the Bitcamp hackathon, 2022
• Volunteer for Girls Talk Math summer camp, 2018 & 2021
• Mentor for Technica hackathon, 2018
• Teaching assistant for Organization of Programming Languages (CMSC 330), University of Maryland, Fall 2017 & Spring 2018
• Teaching assistant for Advanced Programming Principles (CSCI 2041), University of Minnesota, Fall 2014 & Spring 2015

Academic service

• Program committee member for Coq Workshop 2022, PLanQC 2022 & 2024, CPP 2024, ICFP 2024
• Artifact evaluation committee member and external reviewer for OOPSLA 2023 & 2024
• External reviewer for TQC 2020, MFCS 2022, PLDI 2023
• Sub-reviewer for CCS 2017, Oakland S&P 2017, RC 2019, PLDI 2020, QCTIP 2020, PLDI 2021, OOPSLA 2021
• Student volunteer at POPL 2020
• Organizer for the University of Maryland PL reading group, Fall 2018 & Spring 2019