Christine Rizkallah
where else to find them
what they talk about
all 4 in the filters
where they keep going back
- CPP2 editions2022–2025
all 4 in the filters
on a stage with
all 13 in the filters
who talks about the same things
- Ambroise Lafont3 talks
- Adam Chlipala23 talks
- Lennard Gäher7 talks
- Peter Sewell14 talks
- Michael Sammler16 talks
- Cătălin Hriţcu16 talks
| title | conference | date |
|---|---|---|
| Towards Mining Robust Coq Proof Patterns | CoqPL 2025 | 2025-01-25 |
Plans to mine a published Coq dataset for historical breakage and repair patterns, convert Coq scripts into lightweight ASTs, apply tree differencing to… | ||
| Formal Verification of Quantum Stabilizer Code | CoqPL 2025 | 2025-01-25 |
Formalization in Coq of the stabilizer-group algebra and an n‑qubit Pauli/phase construction yields proved algebraic properties (eigenvalues, generators) and a… | ||
| Formalized Burrows-Wheeler Transform | CPP 2025 | 2025-01-20 |
First mechanized verification of the Burrows‑Wheeler transform and its inverse, formalized in Isabelle/HOL and proven correct, invertible, and terminating; two… | ||
| The Cogent and Dargent approach to facilitating verified software development | ICFP 2023 | 2023-09-04 |
Cogent is a restricted functional language with a linear type system and a certifying compiler that emits C, getter/setter code and Isabelle/HOL refinement… | ||
| Dargent: A Silver Bullet for Verified Data Layout Refinement | POPL 2023 | 2023-01-15 |
Dargent provides a declarative layout language integrated into Cogent that generates verified C getters and setters so algebraic types map to bit-precise… | ||
| Overcoming Restraint: Composing Verification of Foreign Functions with Cogent | CPP 2022 | 2022-01-17 |
Cogent’s FFI is proven to preserve uniqueness typing and memory safety while composing Cogent proofs down to C: the compiler’s multi‑phase refinement pipeline… | ||
| nothing matches | ||