Portrait

I am a postdoctoral associate in Computer Science within the CS Department at the Courant Institute of New York University working with Joseph Tassarotti.

Between 2021 and 2024, I was a Ph.D. student within the Cambium team at Inria Paris, in France. I worked under the supervision of Arthur Charguéraud and François Pottier on the formal verification of heap space bounds in the presence of a garbage collector.

Contact: mail

Research interests: functional programming, proof of programs, separation logic, concurrency, space complexity & more.

Publications

All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs.
Alexandre Moine, Sam Westrick, and Joseph Tassarotti.
Submitted, July 2025.
[ PDF ]

TypeDis: A Type System for Disentanglement.
Alexandre Moine, Stephanie Balzer, Alex Xu, and Sam Westrick.
Submitted, July 2025.
[ PDF ]

Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection.
Alexandre Moine, Arthur Charguéraud, and François Pottier.
In ACM Transactions on Programming Languages and Systems, TOPLAS, 2025.
[ PDF | At publisher's | Coq development ]

Ph.D Thesis: Formal Verification of Heap Space Bounds under Garbage Collection.
Alexandre Moine. October 2024.
[ PDF | Long term archive | Coq development | Playlist ]

Snapshottable Stores.
Clément Allain, Basile Clément, Alexandre Moine, and Gabriel Scherer.
In International Conference on Functional Programming, ICFP, 2024. Distinguished Paper Award.
[ PDF | At publisher's | Software | Coq development ]

DisLog: A Separation Logic for Disentanglement.
Alexandre Moine, Sam Westrick, and Stephanie Balzer.
In Principles of Programming Languages, POPL, 2024.
[ PDF | Talk | At publisher's | Coq development ]

A High-Level Separation Logic for Heap Space under Garbage Collection.
Alexandre Moine, Arthur Charguéraud, and François Pottier.
In Principles of Programming Languages, POPL, 2023.
[ PDF | Talk | At publisher's | Extended version | Coq development ]

Specification and Verification of a Transient Stack.
Alexandre Moine, Arthur Charguéraud, and François Pottier.
In International Conference on Certified Programs and Proofs, CPP, 2022. Distinguished Paper Award.
[ PDF | Talk | At publisher's | Coq development ]

Détection de définitions OCaml similaires.
Alexandre Moine and Yann Régis-Gianas.
In Journées Francophones des Langages Applicatifs, JFLA, 2020.
[ PDF ]

Service

Misc

In 2023-2024, I co-organized the PhD Pizza Seminar of Inria Paris.

I was a teaching assistant ("Chargé de TD") for the following undergraduate courses: