Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo. - David Delahaye; Damien Doligez; Frédéric Gilbert 002; Pierre Halmagrand; Olivier Hermant (LPAR, 2013)

Automated Constructivization of Proofs. - Frédéric Gilbert 002 (FoSSaCS, 2017)

Proof Certificates in PVS. - Frédéric Gilbert 002 (ITP, 2017)

Extending higher-order logic with predicate subtyping: Application to PVS. (Extension de la logique d'ordre supérieur avec le sous-typage par prédicats). - Frédéric Gilbert 002 (2018)

Verifiable Certificates for Predicate Subtyping. - Frédéric Gilbert 002 (ESOP, 2019)

Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory. - Ali Assaf 002; Guillaume Burel; Raphaël Cauderlier; David Delahaye; Gilles Dowek; Catherine Dubois; Frédéric Gilbert 002; Pierre Halmagrand; Olivier Hermant; Ronan Saillard (CoRR, 2023)