J. Abrial, The B-Book, Assigning Programs to Meanings, 1996.

J. C. Blanchette, S. Böhme, A. Popescu, and N. Smallbone, Encoding Monomorphic and Polymorphic Types, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp.493-507, 2013.
DOI : 10.1007/978-3-642-36742-7_34
URL : http://arxiv.org/abs/1609.08916

J. C. Blanchette and A. Paskevich, TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
DOI : 10.1007/978-3-642-38574-2_29
URL : https://hal.archives-ouvertes.fr/hal-00825086

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Why3: Shepherd Your Herd of Provers, International Workshop on Intermediate Verification Languages (Boogie), 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

M. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-Calculus Modulo as a Universal Proof Language, Proof Exchange for Theorem Proving (PxTP), pp.28-43, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

R. Bonichon, TaMeD: A Tableau Method for Deduction Modulo, International Joint Conference on Automated Reasoning (IJCAR), pp.445-459, 2004.
DOI : 10.1007/978-3-540-25984-8_33

R. Bonichon, D. Delahaye, and D. Doligez, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), 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, Logic for Programming Phnom Penh (Cambodia), pp.167-181, 2006.

C. E. Brown and G. Smolka, Analytic Tableaux for Simple Type Theory and its First-Order Fragment, Logical Methods in Computer Science, vol.6, issue.2, 2010.
DOI : 10.2168/LMCS-6(2:3)2010

G. Burel, Cut Admissibility by Saturation, Joint International Conference on Rewriting Techniques and Applications and International Conference on Typed Lambda Calculi and Applications (RTA-TLCA), pp.124-138, 2014.
DOI : 10.1007/978-3-319-08918-8_9
URL : https://hal.archives-ouvertes.fr/hal-01097428

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 and D. Delahaye, Integrating Simplex with Tableaux In Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), LNCS, vol.9323, pp.86-101, 2015.

R. Cauderlier and P. Halmagrand, Checking Zenon Modulo Proofs in Dedukti, Proof Exchange for Theorem Proving (PxTP), pp.57-73, 2015.
DOI : 10.4204/EPTCS.186.7
URL : https://hal.archives-ouvertes.fr/hal-01171360

. Clearsy, Atelier B 4.2.1, 2015.

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

D. Delahaye, C. Dubois, C. Marché, and D. Mentré, The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations, Abstract State Machines, Alloy, B, VDM, and Z (ABZ), pp.126-127, 2014.
DOI : 10.1007/978-3-662-43652-3_26
URL : https://hal.archives-ouvertes.fr/hal-00998092

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/hal-01199506

M. Giese, A Calculus for Type Predicates and Type Coercion In Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), LNCS, vol.3702, pp.123-137, 2005.

D. Mentré, C. Marché, J. Filliâtre, and M. Asuka, Discharging Proof Obligations from Atelier??B Using Multiple Automated Provers, Abstract State Machines, Alloy, B, VDM, and Z (ABZ), pp.238-251, 2012.
DOI : 10.1007/978-3-642-30885-7_17

C. Weidenbach, First-Order Tableaux with Sorts, Logic Journal of IGPL, vol.3, issue.6, pp.887-906, 1995.
DOI : 10.1093/jigpal/3.6.887

@. Tptp-tff1, TPTP format for first order logic with polymorphic types)

@. Smt-lib-v2, regular SMT format for many-sorted first order logic)