Publications

Ben Caldwell, William Spencer, Aleks Kissinger, Robert Rand (2026). TensorRocq: Enabling Diagrammatic Reasoning in Rocq. Proceedings of the ACM on Programming Languages.

Cite DOI URL

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

Cite DOI URL

Adrian Lehmann, Ben Caldwell, Bhakti Shah, William Spencer, Robert Rand (2026). VyZX: Formal Verification of a Graphical Quantum Language. ACM Transactions on Programming Languages and Systems (TOPLAS).

Cite DOI arXiv

Youngchan Cho, Robert Rand (2026). Efficiently Verifying Quantum Programs with Few T Gates. Verification, Model Checking, and Abstract Interpretation (VMCAI).

Cite DOI URL

Benjamin Caldwell (2026). Compositionality and Connectivity: Diagrammatic Reasoning in Proof Assistants.

Cite

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

Cite DOI

Adrian Lehmann (2025). Proof Engineering for Quantum Reasoning via E-Graphs.

PDF Cite

Mikhail Mints, Finn Voichick, Leonidas Lampropoulos, Robert Rand (2025). Compositional Quantum Control Flow with Efficient Compilation in Qunity. Object-Oriented Programming, Systems, Languages & Applications (OOPSLA).

Cite DOI URL

Anita Buckley, Pavel Chuprikov, Rodrigo Otoni, Robert Soulé, Robert Rand, Patrick Eugster (2025). A Language for Quantifying Quantum Network Behavior. Object-Oriented Programming, Systems, Languages & Applications (OOPSLA).

Cite DOI URL

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

Cite

Emilio Jesús Gallego Arias, Bhakti Shah (2024). Integrating Dependency Building with Document Checking in Coq. The Tenth International Workshop on Coq for Programming Languages (CoqPL 2024).

PDF

Bhakti Shah (2024). A Lean Formalization of Cedar. Principles of Programming Languages (POPL 2024): Student Research Competition Poster.

PDF Poster

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).

Cite URL

Bhakti Shah (2024). Proof Visualization for Graphical Languages.

Cite

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).

Cite

Anita Buckley, Pavel Chuprikov, Rodrigo Otoni, Robert Rand, Robert Soulé, Patrick Eugster (2024). An Algebraic Language for Specifying Quantum Networks. Proceedings of the ACM on Programming Languages.

Cite DOI URL

Bhakti Shah (2023). Visualizing Graphical Proofs in Coq. International Conference on Functional Programming (ICFP 2023): Student Research Competition Poster.

PDF Poster

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

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.

Cite DOI URL

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

Cite DOI

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

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.

Cite DOI URL

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

Cite URL

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).

Cite arXiv

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

Cite arXiv

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

Cite DOI arXiv URL

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

Cite

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).

Cite

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

Cite

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.

Cite DOI

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

Poster

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. 12th International Conference on Interactive Theorem Proving (ITP 2021).

Cite DOI URL

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

Cite DOI arXiv URL

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. The First International Workshop on Programming Languages for Quantum Computing (PLanQC 2020).

Cite

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

Cite

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

Cite