Time Credits and Time Receipts in Iris. - Glen Mével; Jacques-Henri Jourdan; François Pottier (ESOP, 2019)

Cosmo: a concurrent separation logic for multicore OCaml. - Glen Mével; Jacques-Henri Jourdan; François Pottier (Proc. ACM Program. Lang., 2020)

Formal verification of a concurrent bounded queue in a weak memory model. - Glen Mével; Jacques-Henri Jourdan (Proc. ACM Program. Lang., 2021)

A mechanized program logic for concurrent programs with the weak memory model of Multicore OCaml. (Une logique de programme mécanisée pour les programmes concurrents dans le modèle mémoire faible de Multicore OCaml). - Glen Mével (2022)

Thunks and Debits in Separation Logic with Time Credits. - François Pottier; Armaël Guéneau; Jacques-Henri Jourdan; Glen Mével (Proc. ACM Program. Lang., 2024)