Xavier Leroy
where else to find them
no profile links on file
what they talk about
where they keep going back
- POPL3 editions2021–2026
all 4 in the filters
on a stage with
all 8 in the filters
who talks about the same things
- Gabriel Scherer12 talks
- Peter Sewell14 talks
- Jeremy Yallop12 talks
- Ohad Kammar19 talks
- Nadia Polikarpova24 talks
- Steve Zdancewic19 talks
| title | conference | date |
|---|---|---|
| A Lazy, Concurrent Convertibility Checker | POPL 2026 | 2026-01-11 |
A convertibility algorithm that interleaves evaluation and comparison using lazy channels and concurrent processes, representing lazy values as channels and… | ||
| Mechanizing Abstract Interpretation | N40AI 2024 | 2024-01-20 |
Mechanizes abstract interpretation using Coq and produces an executable analyzer extracted to OCaml; 30,000 lines of Coq implement Verasco with interval… | ||
| Well-founded recursion done right | CoqPL 2024 | 2024-01-20 |
Defines non-structural recursion by adding an extra accessibility proof argument and making recursion structural on that proof, so a function like gcd recurses… | ||
| Panel: Next 50 Years of POPL | POPL 2023 | 2023-01-15 |
Panel discussion surveys POPL's past and future with concrete examples and tensions: cites FlashFill and program synthesis, the 1976 abstract interpretation… | ||
| Verified Code Generation for the Polyhedral Model | POPL 2021 | 2021-01-17 |
A formally verified code generator turns a polyhedral IR into sequential counted loops and is mechanized in Coq producing about 8k lines of development; it… | ||
| Theorem provers are a P.L. researcher's best friend | PLMW @ POPL 2020 | 2020-01-21 |
Argues that mechanized proof shifts PL research from handwavy claims to verifiable artifacts, showing concrete use of Coq and Isabelle/HOL plus SMT solvers to… | ||
| nothing matches | ||