Alexandre Moine
Welcome!
I am a 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 space bounds in the presence of a garbage collector. We use Separation Logic with Space Credits.
Contact: firstname.lastname@inria.fr
.
Research interests: functional programming, proof of programs, separation logic, space complexity & more.
Publications
[1] | 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, Boston, United States, January 2023. [ PDF | At publisher's | Coq development ] |
[2] | 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, Philadelphia, United States, January 2022. Distinguished Paper Award. [ PDF | Talk | At publisher's | Coq development ] |
[3] | Alexandre Moine and Yann Régis-Gianas. Détection de définitions OCaml similaires. In 31ème Journées Francophones des Langages Applicatifs, JFLA, January 2020. [ PDF ] |
Workshop Talks
[1] | 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 ] |