Robert Rand
where else to find them
what they talk about
where they keep going back
all 6 in the filters
on a stage with
all 19 in the filters
who talks about the same things
- Finn Voichick3 talks
- Leonidas Lampropoulos15 talks
- Liyi Li4 talks
- Robert Soulé5 talks
- Pavel Chuprikov5 talks
- Rodrigo Otoni2 talks
| title | conference | date |
|---|---|---|
| Efficiently Verifying Quantum Programs with Few T Gates | VMCAI 2026 | 2026-01-12 |
Mechanized Heisenberg-style logic in the Rocq proof assistant verifies Clifford+T circuits by forwarding conjugation of polystring predicates, targeting… | ||
| Compositional Quantum Control Flow with Efficient Compilation in Qunity | OOPSLA 2025 | 2025-10-16 |
Implementation of the first Qunity compiler that lowers high-level quantum control into OpenQASM 3 and a set of concrete optimizations. Adds two control… | ||
| A Language for Quantifying Quantum Network Behavior | OOPSLA 2025 | 2025-10-16 |
A domain specific language called PBKAT models Bell pair distribution with probabilistic actions (e.g. create succeeds 0.81, swap 0.6) plus nondeterministic… | ||
| Automated Proof Generation for Associative and Distributive Rewriting with E-Graphs | EGRAPHS 2024 | 2024-06-24 |
Encodes a dependently typed DSL for symmetric monoidal categories and the ZX calculus into egglog by computing dependent-type arguments as functions and… | ||
| An Algebraic Language for Specifying Quantum Networks | PLDI 2024 | 2024-06-24 |
Defines BellKAT — a Kleene-algebra based language whose semantics live in a new algebra BellSKA and whose basic primitives are… | ||
| Qunity: A Unified Language for Quantum and Classical Computing | POPL 2023 | 2023-01-15 |
Qunity defines a unified syntax where sum types → direct sum implements operator sums, exception-handling → projective measurement expresses measurements, and… | ||
| Q*: Implementing Quantum Separation Logic in F* | PLanQC 2022 | 2022-09-15 |
Prototype implements quantum separation logic inside F using the Steel library and Z3 for automation, ports Quantum Lib, and adds four quantum actions… | ||
| Extending Gottesman Types Beyond the Clifford Group | PLanQC 2021 | 2021-06-22 |
Extends Gottesman-style types from Clifford-only to universal circuits by adding intersection types plus numeric additive types so T and arbitrary 1‑qubit… | ||
| A Verified Optimizer for Quantum Circuits | POPL 2021 | 2021-01-17 |
VOQC is a fully verified optimizer for quantum circuits implemented in the Coq proof assistant over the SQIR intermediate language; all transformations are… | ||
| Tracking Errors through Types in Quantum Programs | PLanQC 2020 | 2020-01-19 |
A type extension records a natural-number k errors on each qubit and a gate annotation for how many errors it adds; implemented in the embedded quantum… | ||
| nothing matches | ||