I am a PhD student in the Programming Languages Research Group at the University of Pennsylvania, advised by Dr. Steve Zdancewic . My main interest is in formal verification, particularly of probabilistic, nondeterministic and quantum programs. My recent work has revolved around QWIRE ("choir"), a quantum circuit language and verification tool that I developed jointly with Jennifer Paykin.
Publications

Robert Rand, Jennifer Paykin, DongHo Lee, Steve Zdancewic
ReQWIRE: Reasoning about Reversible Quantum Circuits
Quantum Physics and Logic, 2018
[text] 
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

Endre Boros, Vladimir Gurvich, Vladimir Oudalov, Robert Rand
On NashSolvability of ChessLike Games
In stage of submission.
Workshops, Presentations and Posters

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 [slides] 
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 [poster, slides, video] 
Endre Boros, Robert Rand
Terminal Games with Three Terminals Have Proper Nash Equilibria
RUTCOR Research Report, 2009
Teaching
 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