Yann Herklotz
where else to find them
what they talk about
where they keep going back
- CPP2 editions2023–2026
on a stage with
all 8 in the filters
who talks about the same things
- Pepijn de Vos2 talks
- John Wickerson14 talks
- Jose Renau3 talks
- Sara Achour5 talks
- Sylvain Boulmé4 talks
- Adam Chlipala23 talks
| title | conference | date |
|---|---|---|
| Towards composable proofs of cache coherence protocols | CPP 2026 | 2026-01-12 |
Proposes a compositional proof that MSI refines the combination of MI and SI, formalized in Lean 4, cutting required invariants from hundreds to just 15 by… | ||
| Hyperblock Scheduling for Verified High-Level Synthesis | PLDI 2024 | 2024-06-24 |
A verified HLS backend implements a hyperblock scheduler with operation chaining and a system-of-difference-constraints LP scheduler, emits schedules checked… | ||
| 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… | ||
| Formal Verification of High-Level Synthesis | OOPSLA 2021 | 2021-10-17 |
Presents a mechanically verified HLS tool called Vericert that extends CompCert and is proved correct in Coq, translating CompCert 3AC into an HTL FSM and then… | ||
| nothing matches | ||