J. C. Blanchette, S. Böhme, A. Popescu, and N. Smallbone, Encoding monomorphic and polymorphic types. In Tools and Algorithms for the Construction and Analysis of Systems, 2013.

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, S. Conchon, E. Contejean, and S. Lescuyer, Implementing polymorphism in SMT solvers, Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, SMT '08/BPR '08, 2008.
DOI : 10.1145/1512464.1512466

R. Bonichon, D. Delahaye, and D. Doligez, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, Logic for Programming Artificial Intelligence and Reasoning (LPAR, 2007.
DOI : 10.1007/978-3-540-75560-9_13
URL : https://hal.archives-ouvertes.fr/inria-00315920

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, Logic for Programming Artificial Intelligence and Reasoning (LPAR), 2015.
URL : https://hal.archives-ouvertes.fr/hal-01204701

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

S. Cruanes, Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01223502

D. Wand, Polymorphic+Typeclass Superposition, 4th Workshop on Practical Aspects of Automated Reasoning, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01098078