I am an Assistant Professor of Computer Science, part of the Programming Languages Research Group and the Chicago Quantum Exchange.
My main interest is in applying techniques from programming languages and formal verification to the domain of quantum computation. Two of my main projects are the QWIRE quantum circuit language (with Jennifer Paykin) and the VOQC verified optimizing compiler (with Kesha Hietala). I'm currently interested in verified optimization, error-correction, type systems and programming abstractions for quantum computing.
I'm working on a book on verified quantum programming! Email me if you'd like to use the book for your own course.
I'm currently looking for new students at all levels: Please reach out!
Publications 
-
Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks
A Verified Optimizer for Quantum Programs
Principles of Programming Languages, 2021 (distinguished paper)
[full text, paper] -
Robert Rand, Aarthi Sundaram, Kartik Singhal, Brad Lackey
Gottesman Types for Quantum Programs
Quantum Physics and Logic, 2020
[text, slides, video] -
Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks
Verified Optimization in a Quantum Intermediate Representation
Quantum Physics and Logic, 2019 (talk only)
[text, slides] -
Robert Rand, Kesha Hietala, Michael Hicks
Formal Verification vs. Quantum Uncertainty
Summit on Advances in Programming Languages, 2019
[text, slides] -
Robert Rand, Jennifer Paykin, Dong-Ho Lee, Steve Zdancewic
ReQWIRE: Reasoning about Reversible Quantum Circuits
Quantum Physics and Logic, 2018
[text, slides, video] -
Robert Rand, Jennifer Paykin, Steve Zdancewic
QWIRE Practice: Formal Verification of Quantum Circuits in Coq
Quantum Physics and Logic, 2017
[text, slides, video] -
Jennifer Paykin, Robert Rand, Steve Zdancewic
QWIRE: A Core Language for Quantum Circuits
Principles of Programming Languages, 2017.
[text, appendix, slides] -
Robert Rand, Steve Zdancewic
VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs
Mathematical Foundations of Programming Semantics, 2015.
[text, expanded version, slides] -
Kira Adaricheva, James B Nation, Robert Rand
Ordered Direct Implicational Basis of a Finite Closure System
Discrete Applied Mathematics, 2013
Work in Progress
-
Robert Rand, Aarthi Sundaram, Kartik Singhal, Brad Lackey
Static Analysis of Quantum Programs via Gottesman Types
Under submission. -
Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks
Proving Quantum Programs Correct
Under submission.
Workshops, Presentations and Posters
-
Kesha Hietala, Robert Rand, Michael Hicks
Tracking Errors through Types in Quantum Programs
Programming Languages for Quantum Computing, 2020
[text, slides, video] -
Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks
A Verified Optimizer for Quantum Circuits
&
Kartik Singhal, Robert Rand, Michael Hicks
Verified Translation Between Low-Level Quantum Languages
Merged Talk: Programming Languages for Quantum Computing, 2020
[slides, video] -
Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks
Verified Optimization in a Quantum Intermediate Representation
NISQ 2019 Poster -
Robert Rand, Jennifer Paykin, Steve Zdancewic
Phantom Types for Quantum Programs
Coq for Programming Languages, 2018
[extended abstract, slides, video] -
Robert Rand
Formally Verifying Your Quantum Programs
New Jersey Programming Languages and Systems, 2017 -
Robert Rand
Verification Logics for Quantum Programs
Written Preliminary Examination II
[survey, slides, video] -
Jennifer Paykin, Robert Rand, Steve Zdancewic
QWIRE: A QRAM-Inspired Quantum Circuit Language
QPL 2016 Poster Presentation -
Robert Rand, Steve Zdancewic
Models for Probabilistic Programs with an Adversary
Probabilistic Programming Semantics, 2016
[abstract, slides, blog] -
Robert Rand
Verifying Probabilistic Programs in the Presence of an Adversary
ICFP 2015 Poster Presentation (3rd place)
[poster, slides, video] -
Endre Boros, Robert Rand
Terminal Games with Three Terminals Have Proper Nash Equilibria
RUTCOR Research Report, 2009
Teaching
- Instructor, Discrete Mathematics, University of Chicago, Fall 2020
- Instructor, Program Analysis and Understanding, University of Maryland, Spring 2019
- Instructor, Python Programming, University of Pennsylvania, Fall 2015 and Spring 2016
- Teaching Assistant, Introduction to Algorithms, University of Pennsylvania, Spring 2014
- Teaching Assistant, Automata, Computability, and Complexity, University of Pennsylvania, Fall 2013
- Lab Instructor, Introduction to Algorithms, Yeshiva University, Fall 2010
- Recitation Instructor, Discrete Structures, Yeshiva University, Spring 2009 and Spring 2010
Tutorials
- WiSQCE 2020: Quantum Circuits, Verification
- POPL 2020 VQC Tutorial
- POPL 2016 Coq Tutorial
- CUFP 2015 Coq Tutorial
Thesis
- Formally Verified Quantum Programming
PhD Thesis, University of Pennsylvania, 2018.