Reaching for the Star: Tale of a Monad in Coq. - Pierre Nigron; Pierre-Évariste Dagand (ITP, 2021)

Programmes avec effets et leurs preuves dans la théorie des types : application à la compilation certifiée et aux traitements de paquets certifiés. (Effectful programs and their proofs in type theory : application to certified compilation and certified packet processing). - Pierre Nigron (2022)