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)

Implementing Polymorphism in Zenon. - Guillaume Bury; Raphaël Cauderlier; Pierre Halmagrand (IWIL@LPAR, 2015)

Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo. - Guillaume Bury; David Delahaye; Damien Doligez; Pierre Halmagrand; Olivier Hermant (LPAR (short papers), 2015)

Checking Zenon Modulo Proofs in Dedukti. - Raphaël Cauderlier; Pierre Halmagrand (PxTP@CADE, 2015)

Soundly Proving B Method Formulæ Using Typed Sequent Calculus. - Pierre Halmagrand (ICTAC, 2016)

Automated Deduction and Proof Certification for the B Method. (Déduction Automatique et Certification de Preuve pour la Méthode B). - Pierre Halmagrand (2016)

First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice. - Guillaume Burel; Guillaume Bury; Raphaël Cauderlier; David Delahaye; Pierre Halmagrand; Olivier Hermant (J. Autom. Reason., 2020)

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)