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).