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

Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection with Separation Logic.
Alexandre Moine, Arthur Charguéraud, and François Pottier.
Just accepted for publication in TOPLAS, January 2025.
[ PDF | Coq development ]

Ph.D Thesis: Formal Verification of Heap Space Bounds under Garbage Collection.
Alexandre Moine. October 2024.
[ PDF | 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: