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.
Submitted, September 2024.
[ 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 ]

Workshop Talks

Diamonds Are Forever: Reasoning about Heap Space in a Concurrent and Garbage Collected Language.
In The Third Iris Workshop, May 22 2023.
[ Slides ]

Polishing a Rough Diamond: An Enhanced Separation Logic for Heap Space under Garbage Collection.
In Advances in Separation Logics, July 31 2022.
[ Slides ]

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: