S. Bernard, Y. Bertot, L. Rideau, and P. Strub, Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, p.7687, 2016.
DOI : 10.1145/2854065.2854072

S. Boutin, Using Reection to Build Ecient and Certied Decision Procedures, Theoretical Aspects of Computer Software, Third International Symposium, TACS '97 Proceedings, volume 1281 of Lecture Notes in Computer Science, p.515529, 1997.
DOI : 10.1007/bfb0014565

M. Dénès, A. Mörtberg, and V. Siles, A Renement-Based Approach to Computational Algebra in Coq, Interactive Theorem Proving -Third International Conference, ITP 2012 Proceedings, volume 7406 of Lecture Notes in Computer Science, p.8398, 2012.

G. Gonthier, A. Mahboubi, and E. Tassi, A Small Scale Reection Extension for the Coq system, 2015.

C. Keller and M. Lasson, Parametricity in an Impredicative Sort Computer Science Logic (CSL'12) -26th International Workshop, 21st Annual Conference of the EACSL, CSL 2012 Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, p.381395, 2012.

A. Mahboubi and B. Gregoire, Proving Equalities in a Commutative Ring Done Right in Coq
URL : https://hal.archives-ouvertes.fr/hal-00819484

J. C. Reynolds, Types, Abstraction and Parametric Polymorphism, IFIP Congress, p.513523, 1983.

M. Sozeau and N. Oury, First-Class Type Classes, Theorem Proving in Higher Order Logics, 21st International Conference Proceedings, p.278293, 2008.
DOI : 10.1007/11542384_8

URL : https://hal.archives-ouvertes.fr/inria-00628864

P. Wadler, Theorems for free!, Proceedings of the fourth international conference on Functional programming languages and computer architecture , FPCA '89, p.347359, 1989.
DOI : 10.1145/99370.99404