Certifying cost annotations in compilers - Roberto M. Amadio; Nicholas Ayache; Yann Régis-Gianas; Ronan Saillard (CoRR, 2010)

Walking through the Forest: Fast EUF Proof-Checking Algorithms. - Frédéric Besson; Pierre-Emmanuel Cornilleau; Ronan Saillard (PxTP, 2012)

Rewriting Modulo βin the λΠ-Calculus Modulo. - Ronan Saillard (LFMTP, 2015)

Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. (Vérification de typage pour le lambda-Pi-Calcul Modulo : théorie et pratique). - Ronan Saillard (2015)

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)