CV

Education

• Ph.D. in Computer Science, University of Maryland, 2022
  • Dissertation: A Verified Software Toolchain for Quantum Programming
  • Advised by Michael Hicks
• M.S. in Computer Science, University of Maryland, 2019
• B.S. in Computer Science, University of Minnesota, Summa cum laude, 2016
  • Minors in Mathematics and Asian Languages and Literatures (Japanese)

Work experience

I worked at Amazon (AWS) July 2022 - September 2024.

During my time as a student, I was fortunate enough to have 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. "How We Built Cedar: A Verification-Guided Approach." Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering (FSE). 2024.

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. "Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization." Proceedings of the ACM on Programming Languages (OOPSLA). 2024.

A Verified Optimizer for Quantum Circuits (Journal Version)

Kesha Hietala, Robert Rand, Liyi Li, Shih-Han Hung, Xiaodi Wu, Michael Hicks. "A Verified Optimizer for Quantum Circuits." ACM Transactions on Programming Languages and Systems (TOPLAS), 45(3). 2023.

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. "A Formally Certified End-to-end Implementation of Shor’s Factorization Algorithm." Proceedings of the National Academy of Sciences (PNAS). 2023.

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. "FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores." Proceedings of the ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP). 2023.

Verified Compilation of Quantum Oracles

Liyi Li, Finn Voichick, Kesha Hietala, Yuxiang Peng, Xiaodi Wu, Michael Hicks. "Verified Compilation of Quantum Oracles." Proceedings of the ACM on Programming Languages (OOPSLA). 2022.

Q# as a Quantum Algorithmic Language

Kartik Singhal, Kesha Hietala, Sarah Marshall, Robert Rand. "Q# as a Quantum Algorithmic Language." Proceedings of the 19th International Conference on Quantum Physics and Logic (QPL). 2022.

Proving Quantum Programs Correct

Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks. "Proving Quantum Programs Correct." Proceedings of the Conference on Interactive Theorem Proving (ITP). 2021.

A Verified Optimizer for Quantum Circuits

Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks. "A Verified Optimizer for Quantum Circuits." Proceedings of the ACM Conference on Principles of Programming Languages (POPL). 2021.

Finding Substitutable Binary Code By Synthesizing Adapters

Vaibhav Sharma, Kesha Hietala, Stephen McCamant. "Finding Substitutable Binary Code By Synthesizing Adapters." IEEE Transactions on Software Engineering (TSE). 2019.

Formal Verification vs. Quantum Uncertainty

Robert Rand, Kesha Hietala, Michael Hicks. "Formal Verification vs. Quantum Uncertainty." 3rd Summit on Advances in Programming Languages (SNAPL). 2019.

Quantitative Robustness Analysis of Quantum Programs

Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, Xiaodi Wu. "Quantitative Robustness Analysis of Quantum Programs." Proceedings of the ACM Conference on Principles of Programming Languages (POPL). 2019.

Volume-Based Merge Heuristics for Disjunctive Numeric Domains

Andrew Ruef, Kesha Hietala, Arlen Cox. "Volume-Based Merge Heuristics for Disjunctive Numeric Domains." International Static Analysis Symposium (SAS). 2018.

Finding Substitutable Binary Code for Reverse Engineering by Synthesizing Adapters

Vaibhav Sharma, Kesha Hietala, Stephen McCamant. "Finding Substitutable Binary Code for Reverse Engineering by Synthesizing Adapters." 2018 IEEE 11th International Conference on Software Testing, Verification and Validation (ICST). 2018.

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 here). Hopefully this will be expanded to a full paper in the future, but the project is on hold for now.
• Quantum Programming Languages
  Kesha Hietala
  Writeup for a class project, 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

A Verified Software Toolchain for Quantum Programming

Dissertation defense, University of Maryland, College Park, MD, May, 2022

Quantum IRs for Formal Verification

Invited talk, QCE21 Workshop on Quantum Intermediate Representations, Virtual, October, 2021

Proving Quantum Programs Correct

Paper presentation, ITP 2021, Virtual, June, 2021

Expanding the VOQC Toolkit

Extended abstract, PLanQC 2021, Virtual, June, 2021

A Verified Optimizer for Quantum Circuits

Paper presentation, POPL 2021, Virtual, January, 2021

Approaches to Compiling Functional Languages

Seminar presentation, University of Minnesota, Minneapolis, MN, May, 2016

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 & Mentorship

• Project lead for the Tech+Research track at Technica, 2019 & 2022
• 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 (UMD CMSC 330), University of Maryland, Fall 2017 & Spring 2018
• Teaching Assistant for Advanced Programming Principles (UMN CSCI 2041), University of Minnesota, Fall 2014 & Spring 2015

Academic Service

• PC member for Coq Workshop 2022, PLanQC 2022 & 2024, CPP 2024, ICFP 2024
• AEC member & 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 UMD’s PL reading group, Fall 2018 & Spring 2019