SpecCert: Specifying and Verifying Hardware-Based Security Enforcement. - Thomas Letan; Pierre Chifflier; Guillaume Hiet; Pierre Néron; Benjamin Morin (FM, 2016)

Modular Verification of Programs with Effects and Effect Handlers in Coq. - Thomas Letan; Yann Régis-Gianas; Pierre Chifflier; Guillaume Hiet (FM, 2018)

Specifying and Verifying Hardware-based Security Enforcement Mechanisms. (Spécifier et vérifier des stratégies d'application de politiques de sécurité s'appuyant sur des mécanismes matériels). - Thomas Letan (2018)

FreeSpec: specifying, verifying, and executing impure computations in Coq. - Thomas Letan; Yann Régis-Gianas (CPP, 2020)

Modular verification of programs with effects and effects handlers. - Thomas Letan; Yann Régis-Gianas; Pierre Chifflier; Guillaume Hiet (Formal Aspects Comput., 2021)