Postdoc in PL at NYU - I'm proving things correct and efficient using separation logic.
Postdoc in PL at NYU - I'm proving things correct and efficient using separation logic.
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!
Postdoc in PL at NYU - I'm proving things correct and efficient using separation logic.
Takeaway from POPL's business meeting: do parsing.
Postdoc in PL at NYU - I'm proving things correct and efficient using separation logic.
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-
Postdoc in PL at NYU - I'm proving things correct and efficient using separation logic.
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).
Postdoc in PL at NYU - I'm proving things correct and efficient using separation logic.
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 🎉
Postdoc in PL at NYU - I'm proving things correct and efficient using separation logic.
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 )
Postdoc in PL at NYU - I'm proving things correct and efficient using separation logic.
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! )