Publications

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 Slides Video DOI

Robert Rand, Aarthi Sundaram, Kartik Singhal, Brad Lackey (2021). Static Analysis of Quantum Programs via Gottesman Types. arXiv preprint.

PDF Cite arXiv

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

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

PDF Cite