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.
Research interests: functional programming, proof of programs, separation logic, concurrency, space complexity & more.
|||Alexandre Moine, Sam Westrick, and Stephanie Balzer. DisLog: A separation logic for disentanglement. In Principles of Programming Languages, POPL, 2024. [ PDF | Coq development ]|
|||Alexandre Moine, Arthur Charguéraud, and François Pottier. A high-level separation logic for heap space under garbage collection. In Principles of Programming Languages, POPL, 2023. [ PDF | Talk | At publisher's | Coq development ]|
|||Alexandre Moine, Arthur Charguéraud, and François Pottier. Specification and verification of a transient stack. In International Conference on Certified Programs and Proofs, CPP, 2022. Distinguished Paper Award. [ PDF | Talk | At publisher's | Coq development ]|
|||Alexandre Moine and Yann Régis-Gianas. Détection de définitions OCaml similaires. In Journées Francophones des Langages Applicatifs, JFLA, 2020. [ PDF ]|
|||Alexandre Moine. Diamonds are forever: Reasoning about heap space in a concurrent and garbage collected language. In The Third Iris Workshop, May 22 2023. [ Slides ]|
|||Alexandre Moine. Polishing a rough diamond: An enhanced separation logic for heap space under garbage collection. In Advances in Separation Logics, ASL, July 31 2022. [ Slides ]|
TeachingI was a teaching assistant ("Chargé de TD") for the following undergraduate courses:
- Functional Programming (OCaml): Fall 2023
- Automata Theory: Fall 2021, Fall 2022