| A verified optimizer for quantum circuits K Hietala, R Rand, SH Hung, X Wu, M Hicks Proceedings of the ACM on Programming Languages 5 (POPL), 1-29, 2021 | 104 | 2021 |
| Quantitative robustness analysis of quantum programs SH Hung, K Hietala, S Zhu, M Ying, M Hicks, X Wu Proceedings of the ACM on Programming Languages 3 (POPL), 1-29, 2019 | 40 | 2019 |
| Proving quantum programs correct K Hietala, R Rand, SH Hung, L Li, M Hicks arXiv preprint arXiv:2010.01240, 2020 | 34 | 2020 |
| Q# as a quantum algorithmic language K Singhal, K Hietala, S Marshall, R Rand arXiv preprint arXiv:2206.03532, 2022 | 17 | 2022 |
| Verified compilation of quantum oracles L Li, F Voichick, K Hietala, Y Peng, X Wu, M Hicks Proceedings of the ACM on Programming Languages 6 (OOPSLA2), 589-615, 2022 | 13 | 2022 |
| Verified optimization in a quantum intermediate representation K Hietala, R Rand, SH Hung, X Wu, M Hicks arXiv preprint arXiv:1904.06319, 2019 | 12 | 2019 |
| A formally certified end-to-end implementation of Shor’s factorization algorithm Y Peng, K Hietala, R Tao, L Li, R Rand, M Hicks, X Wu Proceedings of the National Academy of Sciences 120 (21), e2218775120, 2023 | 10 | 2023 |
| Formal verification vs. quantum uncertainty R Rand, K Hietala, M Hicks 3rd Summit on Advances in Programming Languages (SNAPL 2019), 2019 | 9 | 2019 |
| Finding substitutable binary code for reverse engineering by synthesizing adapters V Sharma, K Hietala, S McCamant 2018 IEEE 11th International Conference on Software Testing, Verification …, 2018 | 7 | 2018 |
| Finding substitutable binary code by synthesizing adapters V Sharma, K Hietala, S McCamant IEEE Transactions on Software Engineering 47 (8), 1626-1643, 2019 | 5 | 2019 |
| FastVer2: a provably correct monitor for concurrent, key-value stores A Arasu, T Ramananandro, A Rastogi, N Swamy, A Fromherz, K Hietala, ... Proceedings of the 12th ACM SIGPLAN International Conference on Certified …, 2023 | 3 | 2023 |
| Volume-based merge heuristics for disjunctive numeric domains A Ruef, K Hietala, A Cox Static Analysis: 25th International Symposium, SAS 2018, Freiburg, Germany …, 2018 | 3 | 2018 |
| Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version) J Cutler, C Disselkoen, A Eline, S He, K Headley, M Hicks, K Hietala, ... arXiv preprint arXiv:2403.04651, 2024 | 1 | 2024 |
| Cedar: A new language for expressive, fast, safe, and analyzable authorization J Cutler, C Disselkoen, A Eline, S He, K Headley, M Hicks, K Hietala, ... | 1 | 2024 |
| A Verified Optimizer for Quantum Circuits K Hietala, R Rand, L Li, SH Hung, X Wu, M Hicks ACM Transactions on Programming Languages and Systems 45 (3), 1-35, 2023 | 1 | 2023 |
| A Verified Software Toolchain for Quantum Programming K Hietala University of Maryland, College Park, 2022 | 1 | 2022 |
| 12th International Conference on Interactive Theorem Proving (ITP 2021) MO Myreen, N Polikarpova, A Popescu, T Bauereiss, P Lammich, ... Schloss Dagstuhl-Leibniz-Zentrum für Informatik GmbH, 2021 | | 2021 |
| Tracking Errors through Types in Quantum Programs K Hietala, R Rand, M Hicks | | 2019 |
| Detecting Behaviorally Equivalent Functions via Symbolic Execution K Hietala | | 2016 |
| QuantumLib: A Library for Quantum Computing in Coq J Zweifler, K Hietala, R Rand | | |
Robert RandAssistant Professor of Computer Science, University of ChicagoVerified email at uchicago.edu
