I am a Basili Postdoctoral Fellow in Programming Languages at the University of Maryland and the Joint Center for Quantum Information and Computer Science.
My main interest is in applying techniques from programming languages and formal verification to the domain of quantum computation. My PhD thesis revolved around QWIRE ("choir"), a quantum circuit language and verification tool that I developed jointly with Jennifer Paykin at the University of Pennsylvania. I'm currently interested in verified optimization, errorcorrection and programming abstractions for quantum computing.
I'm working on a book on verified quantum programming! I'll be presenting it at POPL in January, email me if you'd like to use the book for your own course.
I'm currently organizing and chairing PLanQC 2020, the First International Workshop on Programming Languages for Quantum Computing! Join us in New Orleans on January 19th (right before POPL).
Publications

Kesha Hietala, Robert Rand, ShihHan Hung, Xiaodi Wu, Michael Hicks
Verified Optimization in a Quantum Intermediate Representation
Quantum Physics and Logic, 2019
[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

Kesha Hietala, Robert Rand, ShihHan Hung, Xiaodi Wu, Michael Hicks
A Verified Optimizer for Quantum Circuits
In stage of submission.
Workshops, Presentations and Posters

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, 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
Thesis
 Formally Verified Quantum Programming
PhD Thesis, University of Pennsylvania, 2018.