Publications

(2021). Toward a Type-Theoretic Interpretation of Q#. International Workshop on Programming Languages for Quantum Computing (PLanQC 2021).

PDF Cite Slides Video

(2021). Extending Gottesman Types Beyond the Clifford Group. International Workshop on Programming Languages for Quantum Computing (PLanQC 2021).

PDF Cite Slides Video

(2021). Expanding the VOQC Toolkit. International Workshop on Programming Languages for Quantum Computing (PLanQC 2021).

PDF Cite Slides Video

(2021). Toward Formalizing the Q# Programming Language. International Conference on Quantum Physics and Logic (QPL 2021) Poster.

PDF Poster

(2021). Proving Quantum Programs Correct. International Conference on Interactive Theorem Proving (ITP 2021).

PDF Cite Video DOI

(2021). A Verified Optimizer for Quantum Circuits. ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2021).

PDF Cite Code Slides Video DOI

(2021). Static Analysis of Quantum Programs via Gottesman Types. arXiv preprint.

PDF Cite arXiv

(2020). Formal Verification of Gottesman Semantics. International Conference on Quantum Physics and Logic (QPL 2021) Poster.

PDF Poster

(2020). Verified translation between low-level quantum languages. International Workshop on Programming Languages for Quantum Computing (PLanQC 2020).

PDF Cite Slides Video

(2020). Tracking Errors through Types in Quantum Programs. International Workshop on Programming Languages for Quantum Computing (PLanQC 2020).

PDF Cite Slides Video

(2020). Gottesman Types for Quantum Programs. International Conference on Quantum Physics and Logic (QPL 2020).

PDF Cite Slides Video

(2020). A Verified Optimizer for Quantum Circuits. International Workshop on Programming Languages for Quantum Computing (PLanQC 2020).

PDF Cite Slides Video

(2019). Verified Optimization in a Quantum Intermediate Representation. Workshop on Noisy Intermediate-Scale Quantum Technologies (NISQ 2020) Poster.

Poster

(2019). Verified Optimization in a Quantum Intermediate Representation. Presented at the International Conference on Quantum Physics and Logic (QPL 2019).

PDF Cite Slides arXiv

(2019). Formal Verification vs. Quantum Uncertainty. Summit on Advances in Programming Languages (SNAPL 2019).

PDF Cite Slides

(2018). Formally Verified Quantum Programming. University of Pennsylvania Dissertations.

PDF Cite Link

(2018). ReQWIRE: Reasoning about Reversible Quantum Circuits. International Conference on Quantum Physics and Logic (QPL 2018).

PDF Cite Code Slides Video DOI

(2018). Phantom Types for Quantum Programs. International Workshop on Coq for Programming Languages (CoqPL 2018).

PDF Cite Slides Video

(2017). QWIRE Practice: Formal Verification of Quantum Circuits in Coq. International Conference on Quantum Physics and Logic (QPL 2017).

PDF Cite Code Slides DOI

(2017). QWIRE: A Core Language for Quantum Circuits. ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017).

PDF Cite Code Slides DOI

(2016). QWIRE: A QRAM-Inspired Quantum Circuit Language. International Conference on Quantum Physics and Logic (QPL 2016) Poster.

Poster

(2016). Verification Logics for Quantum Programs. Written Preliminary Examination II.

PDF Cite Slides Video arXiv

(2016). Models for Probabilistic Programs with an Adversary. Probabilistic Programming Semantics (PPS 2016).

PDF Slides

(2015). VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs. Mathematical Foundations of Programming Semantics (MFPS 2015).

PDF Cite Slides DOI

(2015). Verifying Probabilistic Programs in the Presence of an Adversary. International Conference on Functional Programming (ICFP 2015) Poster.

Slides Video Poster

(2013). Ordered direct implicational basis of a finite closure system. Discrete Applied Mathematics.

PDF Cite

(2009). Terminal games with three terminals have proper Nash equilibria. RUTCOR Research Report.

PDF Cite