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 ramasse-miettes OCaml.

Mon rapport de stage est disponible ici (en anglais).