Research projects

Hamiltonian-oriented Algorithm Design and Programming

• SIMUlation language for Quantum (SIMUQ) (POPL 2024)

• Quantum Hamiltonian Descent

• Hamiltonian Embedding Techniques

• QHD-based OPTimizer (QHDOPT) Software

Infrastructure for Quantum System Engineering

• RISC-Q: a generator for real-time quantum control system-on-chip (SoCs) compatible with RISC-V. See related talks.

A Certified Quantum Software Tool-Chain

• Small Quantum Intermediate Representation (SQIRE) and A Verified Optimizer for Quantum Circuits (POPL 2021).

• A Fully Certified End-to-End Implementation of Shor's Algorithm (PNAS).

• Verified Compilation of Quantum Oracles (OOPSLA 2022).

• Qanfy: a quantum extension of Dafny for automatic reasonings for quantum, classical, and hybrid programs (ECOOP 2024).

Post-Quantum Cryptography: Certification of Security and Implementation

• Formalized Security Proof for Dilithium in the ROM (CRYPTO 2023)

• EasyCrypt for Post-Quantum Cryptography (CCS 2021). (unavailable)

Differentiable Quantum Programming

• A Compiler for Differentiable Quantum Programming Languages (PLDI 2020).

• Differentiable Quantum Programming with Unbounded Loops (ACM TOSEM).

• Differentiable Analog Quantum Programming (NeurIPS 2022).

Practical Verification of Specific Quantum Computing Tasks

• A Scalable Classical Verification of Gaussian Boson Sampling (Website Upcoming!)

• A Circuit Obfuscator for Scalable Verification of Quantum Supremacy.

Meta Programming for Quantum Computing

• A Meta-Programming Framework for Automating NISQ Application Design (ACM TQC).

Quantum Program Synthesis

• A Case for Synthesis of Recursive Quantum Unitary Programs (POPL 2024).

Quantum Machine Learning

• Quantum Wasserstein Generative Adversarial Networks (NeurIPS 2019).