Alexandre Moine

To PhD students: beware of the examples you chose for your presentations, they follow you all your life. I'm using the same example from my very first talk in my job talk!

Takeaway from POPL's business meeting: do parsing.

Glad to announce that our paper "All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs" ( https://arxiv.org/pdf/2511.23283 ) with @shwestrick@discuss.systems and Joseph Tassarotti got a distinguished paper award at POPL'26 🎉

The POPL'26 schedule is out, and I’m thrilled to be giving 3 talks this year! Come and say hi if you're curious about formal verification, separation logic, and concurrency :) I'll be presenting:

* All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs ( https://arxiv.org/pdf/2511.23283 )
* TypeDis: A Type System for Disentanglement ( https://arxiv.org/pdf/2511.23358 )
* Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection (a TOPLAS paper, https://doi.org/10.1145/3716312 )

If you're attending PLMW at POPL next week, and if you're curious about what it is like to live on another continent, come see my talk (from a French in New York). Expect pictures of cats. https://popl26.sigplan.org/details/PLMW-POPL-2026/3/The-Art-of-Living-Abroad-and-Finding-a-Good-Baguette-in-New-York-

It's always fun to read papers from the late 80's. (Apparently, https://doi.org/10.1145/48529.48535 were among the first to reason about spatial locality --- still relevant today! )

Today I came across what seems to be a cool new workshop, co-located with ETAPS'26: AnalyzeThat ( https://analyzethat.gitlab.io/ ). It will focus on static verification _in a limited time_ of open source projects, to challenge heavily-automated verification frameworks (and hence complement challenges such as VerifyThis, focused on deductive/more manual verification).