M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry et al., A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, Lecture Notes in Computer Science, vol.53, issue.6, pp.135-150, 2011.
DOI : 10.1145/1217856.1217859
URL : https://hal.archives-ouvertes.fr/hal-00639130

R. Atkey, A deep embedding of parametric polymorphism in Coq, Workshop on Mechanizing Metatheory, 2009.

R. Atkey, Syntax for Free: Representing Syntax with Binding Using Parametricity, Lecture Notes in Computer Science, vol.18, issue.1, pp.35-49, 2009.
DOI : 10.1017/S0956796807006557

J. Bernardy and M. Lasson, Realizability and Parametricity in Pure Type Systems, Lecture Notes in Computer Science, vol.6604, pp.108-122, 2011.
DOI : 10.1007/978-3-642-19805-2_8
URL : https://hal.archives-ouvertes.fr/hal-00589893

T. Coquand, An Analysis of Girard's Paradox, LICS, pp.227-236, 1986.

T. Coquand and C. Paulin, Inductively defined types, Conference on Computer Logic, pp.50-66, 1988.
DOI : 10.1007/3-540-52335-9_47

F. Garillot, Generic Proof Tools and Finite Group Theory, 2011.
URL : https://hal.archives-ouvertes.fr/pastel-00649586

H. Geuvers, Inconsistency of classical logic in type theory Unpublished notes, 11 Eduardo Giménez. Codifying Guarded Definitions with Recursive Schemes. Types for proofs and Programs, pp.39-59, 1995.

G. Gonthier, A. Mahboubi, L. Rideau, E. Tassi, and L. Théry, A Modular Formalisation of Finite Group Theory, Lecture Notes in Computer Science, vol.4732, 2007.
DOI : 10.1007/978-3-540-74591-4_8
URL : https://hal.archives-ouvertes.fr/inria-00139131

B. Grégoire and A. Mahboubi, Proving Equalities in a Commutative Ring Done Right in Coq, Lecture Notes in Computer Science, vol.3603, pp.98-113, 2005.
DOI : 10.1007/11541868_7

L. 14-benjamin-grégoire, B. Théry, and . Werner, A Computational Approach to Pocklington Certificates in Type Theory, Functional and Logic Programming, 2006.

P. Letouzey, A New Extraction for Coq, TYPES, volume 2646 of Lecture Notes in Computer Science, pp.200-219, 2002.
DOI : 10.1007/3-540-39185-1_12
URL : https://hal.archives-ouvertes.fr/hal-00150914

P. Letouzey, Programmation fonctionnelle certifiée: L'extraction de programmes dans l'assistant Coq, 2004.

P. Letouzey, Extraction in Coq: An Overview, CiE, pp.359-369, 2008.
DOI : 10.1007/978-3-540-69407-6_39
URL : https://hal.archives-ouvertes.fr/hal-00338973

. Norell, Towards a Practical Programming Language Based on Dependent Type Theory, 2007.

C. Paulin-mohring, Extracting F(omega)'s Programs from Proofs in the Calculus of Constructions, POPL, pp.89-104, 1989.

C. Paulin-mohring, Inductive definitions in the system Coq rules and properties, Typed Lambda Calculi and Applications, pp.328-345, 1993.
DOI : 10.1007/BFb0037116

D. Gordon, M. Plotkin, and . Abadi, A Logic for Parametric Polymorphism, Lecture Notes in Computer Science, vol.664, pp.361-375, 1993.

C. John and . Reynolds, Types, Abstraction and Parametric Polymorphism, IFIP Congress, pp.513-523, 1983.

I. Takeuti, An Axiomatic System of Parametricity 24 The Coq Development Team. The Coq Proof Assistant: Reference Manual. INRIA, 2012. 25 Dimitrios Vytiniotis and Stephanie Weirich. Parametricity, Type Equality, and Higher- Order Polymorphism, Fundam. Inform. Journal of Functional Programming, vol.33, issue.402, pp.20175-210, 1998.

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