Ordered direct implicational basis of a finite closure system. - Kira V. Adaricheva; James B. Nation; Robert Rand 001 (Discret. Appl. Math., 2013)

VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs. - Robert Rand 001; Steve Zdancewic (MFPS, 2015)

QWIRE: a core language for quantum circuits. - Jennifer Paykin; Robert Rand 001; Steve Zdancewic (POPL, 2017)

QWIRE Practice: Formal Verification of Quantum Circuits in Coq. - Robert Rand 001; Jennifer Paykin; Steve Zdancewic (QPL, 2017)

ReQWIRE: Reasoning about Reversible Quantum Circuits. - Robert Rand 001; Jennifer Paykin; Dong-Ho Lee; Steve Zdancewic (QPL, 2018)

Formal Verification vs. Quantum Uncertainty. - Robert Rand 001; Kesha Hietala; Michael Hicks 001 (SNAPL, 2019)

Verification Logics for Quantum Programs. - Robert Rand 001 (CoRR, 2019)

Verified Optimization in a Quantum Intermediate Representation. - Kesha Hietala; Robert Rand 001; Shih-Han Hung; Xiaodi Wu 001; Michael Hicks 001 (CoRR, 2019)

Gottesman Types for Quantum Programs. - Robert Rand 001; Aarthi Sundaram; Kartik Singhal 002; Brad Lackey (QPL, 2020)

Proving Quantum Programs Correct. - Kesha Hietala; Robert Rand 001; Shih-Han Hung; Liyi Li 002; Michael Hicks 001 (ITP, 2021)

Static Analysis of Quantum Programs via Gottesman Types. - Robert Rand 001; Aarthi Sundaram; Kartik Singhal 002; Brad Lackey (CoRR, 2021)

A verified optimizer for Quantum circuits. - Kesha Hietala; Robert Rand 001; Shih-Han Hung; Xiaodi Wu 001; Michael Hicks 001 (Proc. ACM Program. Lang., 2021)

Writing and verifying a Quantum optimizing compiler (keynote). - Robert Rand 001 (CC, 2022)

A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm. - Yuxiang Peng; Kesha Hietala; Runzhou Tao; Liyi Li 002; Robert Rand 001; Michael Hicks 001; Xiaodi Wu 001 (CoRR, 2022)

Qunity: A Unified Language for Quantum and Classical Computing. - Finn Voichick; Robert Rand 001; Michael W. Hicks (CoRR, 2022)

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

Q# as a Quantum Algorithmic Language. - Kartik Singhal 002; Kesha Hietala; Sarah Marshall; Robert Rand 001 (QPL, 2022)

Advances in Quantum Computation and Quantum Technologies: A Design Automation Perspective. - Giovanni De Micheli; Jie-Hong R. Jiang; Robert Rand 001; Kaitlin N. Smith; Mathias Soeken (IEEE J. Emerg. Sel. Topics Circuits Syst., 2022)

MCBeth: A Measurement-based Quantum Programming Language. - Aidan Evans; Seun Omonije; Robert Soulé; Robert Rand 001 (Q-SE@ICSE, 2023)

Towards an Algebraic Specification of Quantum Networks. - Anita Buckley; Pavel Chuprikov; Rodrigo Otoni; Robert Rand 001; Robert Soulé; Patrick Eugster (QuNet@SIGCOMM, 2023)

Shorter Pulses, Smaller Errors: Quantum Circuit Optimization via Parameterized Pulses. - Finn Voichick; Leonidas Lampropoulos; Robert Rand 001 (CoRR, 2023)

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

Qunity: A Unified Language for Quantum and Classical Computing. - Finn Voichick; Liyi Li 002; Robert Rand 001; Michael Hicks 001 (Proc. ACM Program. Lang., 2023)

A Verified Optimizer for Quantum Circuits. - Kesha Hietala; Robert Rand 001; Liyi Li 002; Shih-Han Hung; Xiaodi Wu 001; Michael Hicks 001 (ACM Trans. Program. Lang. Syst., 2023)

ViCAR: Visualizing Categories with Automated Rewriting in Coq. - Bhakti Shah; William Spencer; Laura Zielinski; Ben Caldwell; Adrian Lehmann; Robert Rand 001 (CoRR, 2024)

An Algebraic Language for Specifying Quantum Networks. - Anita Buckley; Pavel Chuprikov; Rodrigo Otoni; Robert Soulé; Robert Rand 001; Patrick Eugster (Proc. ACM Program. Lang., 2024)

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