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, errorcorrection, 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, ShihHan 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, ShihHan 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, DongHo 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 PartialCorrectness 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, ShihHan 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, ShihHan Hung, Xiaodi Wu, Michael Hicks
A Verified Optimizer for Quantum Circuits
&
Kartik Singhal, Robert Rand, Michael Hicks
Verified Translation Between LowLevel Quantum Languages
Merged Talk: Programming Languages for Quantum Computing, 2020
[slides, video] 
Kesha Hietala, Robert Rand, ShihHan 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 QRAMInspired 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.