Publications

Youngchan Cho, Robert Rand (2025). Verification of Low T-count Quantum Circuits in Rocq.

Cite

Adrian Lehmann, Robert Rand (2025). Domain-Specific Rocq Automation with E-Graphs.

Cite

Mikhail Mints, Finn Voichick, Leonidas Lampropoulos, Robert Rand (2025). Compositional Quantum Control Flow with Efficient Compilation in Qunity.

PDF Cite Code

Anita Buckley, Pavel Chuprikov, Rodrigo Otoni, Robert Rand, Robert Soulé, Patrick Eugster (2025). A Language for Quantifying Quantum Network Behavior.

PDF Cite

Bhakti Shah, William Spencer, Laura Zielinski, Ben Caldwell, Adrian Lehmann, Robert Rand (2024). ViCAR: Visualizing Categories with Automated Rewriting in Coq. The 7th International Conference on Applied Category Theory (ACT).

PDF Cite Code

Finn Voichick, Leonidas Lampropoulos, Robert Rand (2024). COGNAC: Circuit Optimization via Gradients and Noise-Aware Compilation.

Cite DOI arXiv

Adrian Lehmann, Ben Caldwell, John Reppy, Robert Rand (2024). Automated Proof Generation for Associative and Distributive Rewriting with E-Graphs. E-Graph Research, Applications, Practices, and Human-factors (EGRAPHS).

PDF Cite Video

Anita Buckley, Pavel Chuprikov, Rodrigo Otoni, Robert Rand, Robert Soulé, Patrick Eugster (2024). An Algebraic Language for Specifying Quantum Networks. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2024).

Cite

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

Cite DOI URL

Yuxiang Peng, Kesha Hietala, Runzhou Tao, Liyi Li, Robert Rand, Michael Hicks, Xiaodi Wu (2023). A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm. Proceedings of the National Academy of Sciences (PNAS).

Cite Code DOI arXiv

Adrian Lehmann, Ben Caldwell, Bhakti Shah, Robert Rand (2023). VyZX: Formal Verification of a Graphical Quantum Language.

Cite DOI arXiv

Anita Buckley, Pavel Chuprikov, Rodrigo Otoni, Robert Rand, Robert Soulé, Patrick Eugster (2023). Towards an Algebraic Specification of Quantum Networks. Proceedings of the 1st Workshop on Quantum Networks and Distributed Quantum Computing.

PDF Cite DOI URL

Finn Voichick, Liyi Li, Robert Rand, Michael Hicks (2023). Qunity: A Unified Language for Quantum and Classical Computing. ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023).

Cite DOI arXiv URL

Aidan Evans, Seun Omonije, Robert Soulé, Robert Rand (2023). MCBeth: A Measurement-based Quantum Programming Language. 2023 IEEE/ACM 4th International Workshop on Quantum Software Engineering (Q-SE).

Cite Video DOI arXiv

Aarthi Sundaram, Robert Rand, Kartik Singhal, Brad Lackey (2023). Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs. Preprint.

PDF Cite

Kartik Singhal, Robert Rand, Matthew Amy (2022). Beyond Separation: Toward a Specification Language for Modular Reasoning about Quantum Programs. Programming Languages for Quantum Computing (PLanQC 2022) Poster Session.

PDF Cite Poster

Kesha Hietala, Sarah Marshall, Robert Rand, Nikhil Swamy (2022). Q*: Implementing Quantum Separation Logic in F*. The Third International Workshop on Programming Languages for Quantum Computing (PLanQC 2022).

PDF Cite Code Slides Video

Giovanni De Micheli, Jie-Hong R. Jiang, Robert Rand, Kaitlin Smith, Mathias Soeken (2022). Advances in Quantum Computation and Quantum Technologies: A Design Automation Perspective. IEEE Journal on Emerging and Selected Topics in Circuits and Systems.

PDF Cite DOI

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

PDF Cite Code Slides Video DOI arXiv

Adrian Lehmann, Ben Caldwell, Robert Rand (2022). VyZX: A Vision for Verifying the ZX Calculus.

PDF Cite Poster Video arXiv

Jacob Zweifler, Kesha Hietala, Robert Rand (2022). QuantumLib: A Library for Quantum Computing in Coq. The Coq Workshop 2022.

PDF Cite Code Slides

Aarthi Sundaram, Robert Rand, Kartik Singhal, Brad Lackey (2022). A Rich Type System for Quantum Programs.

Cite Poster DOI arXiv

Kartik Singhal, Sarah Marshall, Kesha Hietala, Robert Rand (2021). Toward a Type-Theoretic Interpretation of Q#. International Workshop on Programming Languages for Quantum Computing (PLanQC 2021).

PDF Cite Slides Video

Robert Rand, Aarthi Sundaram, Kartik Singhal, Brad Lackey (2021). Extending Gottesman Types Beyond the Clifford Group. International Workshop on Programming Languages for Quantum Computing (PLanQC 2021).

PDF Cite Slides Video

Kesha Hietala, Liyi Li, Akshaj Gaur, Aaron Green, Robert Rand, Xiaodi Wu, Michael Hicks (2021). Expanding the VOQC Toolkit. International Workshop on Programming Languages for Quantum Computing (PLanQC 2021).

PDF Cite Slides Video

Sarah Marshall, Kartik Singhal, Kesha Hietala, Robert Rand (2021). Toward Formalizing the Q# Programming Language. International Conference on Quantum Physics and Logic (QPL 2021) Poster.

PDF Poster

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

PDF Cite Video DOI

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

PDF Cite Code Poster Slides Video DOI

Jacob Zweifler, Robert Rand (2020). Formal Verification of Gottesman Semantics. International Conference on Quantum Physics and Logic (QPL 2021) Poster.

PDF Poster

Kartik Singhal, Robert Rand, Michael Hicks (2020). Verified translation between low-level quantum languages. International Workshop on Programming Languages for Quantum Computing (PLanQC 2020).

PDF Cite Slides Video

Kesha Hietala, Robert Rand, Michael Hicks (2020). Tracking Errors through Types in Quantum Programs. International Workshop on Programming Languages for Quantum Computing (PLanQC 2020).

PDF Cite Slides Video

Robert Rand, Aarthi Sundaram, Kartik Singhal, Brad Lackey (2020). Gottesman Types for Quantum Programs. International Conference on Quantum Physics and Logic (QPL 2020).

PDF Cite Slides Video

Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks (2020). A Verified Optimizer for Quantum Circuits. International Workshop on Programming Languages for Quantum Computing (PLanQC 2020).

PDF Cite Slides Video

Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks (2019). Verified Optimization in a Quantum Intermediate Representation. Workshop on Noisy Intermediate-Scale Quantum Technologies (NISQ 2020) Poster.

Poster

Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks (2019). Verified Optimization in a Quantum Intermediate Representation. Presented at the International Conference on Quantum Physics and Logic (QPL 2019).

PDF Cite Slides arXiv

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

PDF Cite Slides

Robert Rand (2018). Formally Verified Quantum Programming. University of Pennsylvania Dissertations.

PDF Cite Link

Robert Rand, Jennifer Paykin, Dong-Ho Lee, Steve Zdancewic (2018). ReQWIRE: Reasoning about Reversible Quantum Circuits. International Conference on Quantum Physics and Logic (QPL 2018).

PDF Cite Code Slides Video DOI

Robert Rand, Jennifer Paykin, Steve Zdancewic (2018). Phantom Types for Quantum Programs. International Workshop on Coq for Programming Languages (CoqPL 2018).

PDF Cite Slides Video

Robert Rand, Jennifer Paykin, Steve Zdancewic (2017). QWIRE Practice: Formal Verification of Quantum Circuits in Coq. International Conference on Quantum Physics and Logic (QPL 2017).

PDF Cite Code Slides DOI

Jennifer Paykin, Robert Rand, Steve Zdancewic (2017). QWIRE: A Core Language for Quantum Circuits. ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017).

PDF Cite Code Slides DOI

Jennifer Paykin, Robert Rand, Steve Zdancewic (2016). QWIRE: A QRAM-Inspired Quantum Circuit Language. International Conference on Quantum Physics and Logic (QPL 2016) Poster.

Poster

Robert Rand (2016). Verification Logics for Quantum Programs. Written Preliminary Examination II.

PDF Cite Slides Video arXiv

Robert Rand, Steve Zdancewic (2016). Models for Probabilistic Programs with an Adversary. Probabilistic Programming Semantics (PPS 2016).

PDF Slides

Robert Rand, Steve Zdancewic (2015). VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs. Mathematical Foundations of Programming Semantics (MFPS 2015).

PDF Cite Slides DOI

Robert Rand (2015). Verifying Probabilistic Programs in the Presence of an Adversary. International Conference on Functional Programming (ICFP 2015) Poster.

Slides Video Poster

Kira Adaricheva, James B Nation, Robert Rand (2013). Ordered direct implicational basis of a finite closure system. Discrete Applied Mathematics.

PDF Cite

Robert Noah Rand (2011). Ordered Directness and Efficiently Computing Closures.

Cite

Endre Boros, Robert Rand (2009). Terminal games with three terminals have proper Nash equilibria. RUTCOR Research Report.

PDF Cite