A categorical framework for effects in Coq. (L3 internship)
Partie Coq du projet logique de 2017
implémentation de la KAM dans le cadre du stage de L3 (en Ocaml puis en C)
Program logic for developing and verifying distributed systems