Portrait

I am a postdoctoral associate within the CS Department at the Courant Institute of New York University working with Joseph Tassarotti. Between 2021 and 2024, I was a PhD student within the Cambium team at Inria Paris, working under the supervision of Arthur Charguéraud and François Pottier.

My research focuses on programming languages and formal verification. I aim to prove that programs are both correct and efficient. Currently, I investigate efficiency properties of parallel programs. During my PhD, I developed a program logic for establishing heap space bounds under garbage collection.

Contact: mail

Research interests: verification, separation logic, concurrency, time and 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.
POPL 2026.
[ PDF | Coq development ]

TypeDis: A Type System for Disentanglement.
Alexandre Moine, Stephanie Balzer, Alex Xu, and Sam Westrick.
POPL 2026.
[ PDF | Coq development ]

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

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

DisLog: A Separation Logic for Disentanglement.
Alexandre Moine, Sam Westrick, and Stephanie Balzer.
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.
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.
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.
JFLA 2020.
[ PDF | Software ]

Dissertation

Formal Verification of Heap Space Bounds under Garbage Collection.
Alexandre Moine.
Université Paris Cité / Inria, October 2024.
[ PDF | Long term archive | Coq development | Playlist ]

Service

Misc

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

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