Thibaut Pérami
where else to find them
what they talk about
where they keep going back
- POPL2 editions2024–2026
on a stage with
all 9 in the filters
who talks about the same things
- Zongyuan Liu3 talks
- Angus Hammond3 talks
- Thomas Bauereiss3 talks
- Brian Campbell5 talks
- Peter Sewell14 talks
- Armaël Guéneau7 talks
| title | conference | date |
|---|---|---|
| ArchSem: Reusable Rigorous Semantics of Relaxed Architectures | POPL 2026 | 2026-01-11 |
A reusable framework composes ISA pseudo-code from Sail with concurrency interpreters in Rock via a freemonad of 15 algebraic effects, ingesting the full ARM… | ||
| Towards general white-box automation: a typeclass-guided context cleaner | CoqPL 2025 | 2025-01-25 |
Built a small Ltac2 clarifier called cdestruct that uses typeclass-guided hints to run only safe, non‑backtracking context cleanup: case splits… | ||
| System-level weak memory models: The need for formalisation, ISA semantics integ... | The Future of Weak Memory 2024 | 2024-01-15 |
Argues for fully formalised system-level weak memory models and presents an executable Coq/ROCK-style library that composes a full instruction-set semantics… | ||
| An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: T... | POPL 2024 | 2024-01-14 |
Claims a new separation logic AxSL for the Arm‑A user‑mode axiomatic model that lets relaxed reads/writes transfer resources when they induce ordering… | ||
| nothing matches | ||