Sandrine Blazy
where else to find them
what they talk about
where they keep going back
on a stage with
all 11 in the filters
who talks about the same things
- David Pichardie8 talks
- Aurèle Barrière7 talks
- Olivier Flückiger7 talks
- Adam Chlipala23 talks
- Manas Thakur9 talks
- Jan Vitek26 talks
| title | conference | date |
|---|---|---|
| Towards Verifiable System Code using a DSL Compiled to Efficient and Readable C Code | LCTES 2026 | 2026-06-15 |
A minimal, purely functional DSL called Barocq compiles via Rocq to readable C by enforcing a strict alias-control discipline so the compiler does zero-cost… | ||
| Business Meeting | CPP 2025 | 2025-01-20 |
About 51 papers are submitted and 20 accepted this year, reviewed by 32 PC members with 26 external reviewers and two months for reviews and rebuttals; reviews… | ||
| CompCert: a journey through the landscape of mechanized semantics for verified co... | CPP 2023 | 2023-01-16 |
CompCert implements 18 verified compiler passes across 11 formally‑specified languages and proves semantics preservation by composable small-step semantics and… | ||
| Mechanised Semantics for Gated Static Single Assignment | CPP 2023 | 2023-01-16 |
Provides a formal, mechanised semantics for Gated Static Single Assignment mechanised in Coq and clarifies the role of gamma and eta gates with a… | ||
| Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCe... | POPL 2023 | 2023-01-15 |
Prototype JIT is implemented and mechanically verified in Coq, reusing the CompCert backend and its correctness proofs to generate x86 code, and modeling… | ||
| Formally Verified Speculation and Deoptimization in a JIT Compiler | POPL 2021 | 2021-01-17 |
A formal model defines a JIT’s middle end, an RTL-like IR and two concrete speculative ops: the anchor instruction which marks safe deoptimization points and… | ||
| nothing matches | ||