J. R. Abrial, The B-book: Assigning Programs to Meanings, 1996.
DOI : 10.1017/CBO9780511624162

M. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-calculus modulo as a universal proof language, PxTP 2012, Proceedings, pp.28-43, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

R. Bonichon, TaMeD: A Tableau Method for Deduction Modulo, 2004.
DOI : 10.1007/978-3-540-25984-8_33
URL : https://hal.archives-ouvertes.fr/hal-01520537

R. Bonichon, D. Delahaye, and D. Doligez, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, LNCS, vol.4790, pp.151-165, 2007.
DOI : 10.1007/978-3-540-75560-9_13
URL : https://hal.archives-ouvertes.fr/inria-00315920

R. Bonichon and O. Hermant, A semantic completeness proof for tableaux modulo, LPAR 2006, pp.167-181
DOI : 10.1007/11916277_12
URL : http://www.lix.polytechnique.fr/~hermant/SemanticTableauxModulo.pdf

G. Burel, Embedding Deduction Modulo into a Prover, LNCS, vol.6247, pp.155-169, 2010.
DOI : 10.1007/978-3-642-15205-4_15
URL : http://www.ensiie.fr/~guillaume.burel/download/burel10embedding.pdf

G. Burel and C. Kirchner, Regaining cut admissibility in deduction modulo using abstract completion, Information and Computation, vol.208, issue.2, pp.140-164, 2010.
DOI : 10.1016/j.ic.2009.10.005
URL : https://hal.archives-ouvertes.fr/inria-00132964

G. Bury, D. Delahaye, D. Doligez, P. Halmagrand, and O. Hermant, Automated deduction in the B set theory using typed proof search and deduction modulo
DOI : 10.29007/14v7
URL : https://hal.archives-ouvertes.fr/hal-01204701

A. Fehnker, A. Mciver, G. Sutcliffe, and A. Voronkov, LPAR 2015 ? Short presentations, pp.42-58, 2015.

Z. Chihani, D. Miller, and F. Renaud, A Semantic Framework for Proof Evidence, Journal of Automated Reasoning, vol.42, issue.1, pp.287-330, 2017.
DOI : 10.1017/CBO9781139168717
URL : https://hal.archives-ouvertes.fr/hal-01390912

D. Cousineau, D. Doligez, L. Lamport, S. Merz, D. Ricketts et al., TLA???+??? Proofs, LNCS, vol.2012, issue.7436, pp.147-154, 2012.
DOI : 10.1007/978-3-642-32759-9_14
URL : https://hal.archives-ouvertes.fr/hal-00726631

D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, and O. Hermant, Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo, LPAR 2013, pp.274-290, 2013.
DOI : 10.1007/978-3-642-45221-5_20
URL : https://hal.archives-ouvertes.fr/hal-00909784

G. Dowek, Polarized deduction modulo, In: IFIP Theoretical Computer Science, 2010.
DOI : 10.1007/978-3-642-15240-5_14
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-642-15240-5_14.pdf

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/inria-00077199

C. Dubois and R. Rioboo, Verified Functional Iterators Using the FoCaLiZe Environment, SEFM 2014, pp.317-331, 2014.
DOI : 10.1007/978-3-319-10431-7_26
URL : https://hal.archives-ouvertes.fr/hal-01126458

D. Miller, Foundational proof certificates All about Proofs, Proofs for All, Studies in Logic, Mathematical Logic and Foundations, vol.55, issue.8, pp.150-163, 2015.
DOI : 10.1145/2503887.2503894

A. Nerode and R. A. Shore, Logic for Applications, 1993.

A. Nonnengart and C. Weidenbach, Computing Small Clause Normal Forms, pp.335-367, 2001.
DOI : 10.1016/B978-044450813-3/50008-4
URL : http://www.dfki.de/vse/papers/nrw98.ps.gz

. The-bware and . Project, , 2012.