Kesha Hietala
where else to find them
what they talk about
all 4 in the filters
where they keep going back
- PLanQC3 editions2020–2022
all 4 in the filters
on a stage with
all 26 in the filters
who talks about the same things
- Xiaodi Wu4 talks
- Robert Rand11 talks
- Oded Padon11 talks
- Michael Hicks18 talks
- Adam Chlipala23 talks
- Sara Achour5 talks
| title | conference | date |
|---|---|---|
| Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization | OOPSLA 2024 | 2024-10-20 |
Cedar defines a concise DSL, a Rust evaluation engine, and a Lean formal model that proves key properties; policies compile into SMT in the sound and complete… | ||
| FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores | CPP 2023 | 2023-01-16 |
FastVer2 is a verified, concurrent monitor for the Faster key-value store: implemented in C (≈8,000 lines produced from ≈50,000 lines of F proofs) using the… | ||
| 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… | ||
| Expanding the VOQC Toolkit | PLanQC 2021 | 2021-06-22 |
Vox is a Coq-verified quantum optimizer: every transformation has a formal proof of semantic preservation and some helper proofs (the U3 combination routine is… | ||
| 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… | ||
| A Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum Languages | PLanQC 2020 | 2020-01-19 |
A verified optimizer named Box implements peephole rules (X/Z propagation, gate cancellation) plus rotation‑merging and a naive swap‑based mapper, all… | ||
| nothing matches | ||