Portrait

I am a third year Ph.D. student in Computer Science within the Cambium team at Inria Paris, in France.

I work 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. We use separation logic with space credits.

Contact: mail

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

Publications

[1] 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, April 2024.
[ PDF | Coq development ]
[2] Snapshottable stores. Clément Allain, Basile Clément, Alexandre Moine, and Gabriel Scherer. Submitted, February 2024.
[ PDF ]
[3] 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 ]
[4] 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 ]
[5] 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 ]
[6] 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

[1] Diamonds Are Forever: Reasoning about Heap Space in a Concurrent and Garbage Collected Language. In The Third Iris Workshop, May 22 2023.
[ Slides ]
[2] Polishing a Rough Diamond: An Enhanced Separation Logic for Heap Space under Garbage Collection. In Advances in Separation Logics, July 31 2022.
[ Slides ]

Misc

I co-organize the PhD Pizza Seminar of Inria Paris.

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