Alexandre Moine
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.
Starting October 2024, I will be a postdoctoral associate in the CS Department at the Courant Institute of New York University working with Joseph Tassarotti.
Contact:
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 ]
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:
- Functional Programming (OCaml): Fall 2023
- Automata Theory: Fall 2021, Fall 2022