melocoton
est un projet de
formalisation de l’interopérabilité entre OCaml et C réalisée en Coq avec
la bibliothèque de logique de séparation Iris
.
J’y ai travaillé pendant mon stage de M1 sur l’implémentation des racines locales du GC OCaml.
Mon rapport de stage est disponible ici (en anglais).