P. Aczel and &. Michael-rathjen, Notes on constructive set theory, 2000.

T. Altenkirch, N. A. Danielsson, A. , and N. Oury, ??: Dependent Types without the Sugar. Functional and Logic, 2005.

M. Armand, B. Grégoire, A. Spiwack, and &. Laurent-théry, Extending Coq with Imperative Features and its Application to SAT Verification. Interactive Theorem Proving, pp.83-98, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00502496

A. Asperti, W. Ricotti, C. Sacerdoti, and &. Tassi, A new type for tactics, p.22, 2009.

L. Augustsson, T. , and B. Nordström, A short description of another logical framework, Proceedings of the First Workshop on Logical Frameworks, pp.39-42, 1990.

J. Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.613-641, 1978.
DOI : 10.1145/359576.359579

E. Bishop, Foundations of constructive analysis, 1967.

F. Blanqui and J. Okada, The Calculus of Algebraic Constructions Rewriting Techniques and Applications, volume 1631 of Lecture Notes in Computer Science, 1999.

M. Boespflug, Conversion by Evaluation, Practical Aspects of Declarative Languages: 12th International Symposium, PADL 2010 Proceedings, p. 58, 2010.
DOI : 10.1007/978-3-642-11503-5_7
URL : https://hal.archives-ouvertes.fr/inria-00434282

E. Brady, Practical Implementation of a Dependently Typed Functional Programming Language, 2005.

&. Sylvain-conchon and . Jean-christophe-filliâtre, A persistent union-find data structure, Proceedings of the 2007 workshop on Workshop on ML -ML '07, p.37, 2007.

&. Thierry-coquand and . Spiwack, Towards constructive homological algebra in type theory Towards Mechanized Mathematical Assistants , Lecture Notes in Computer Science, 2007.

R. Edsko-de-vries, &. Plasmeijer, and . David-abrajamson, Uniqueness typing simplified Implementation and Application of Functional Languages, Lecture Notes in Computer Science, vol.0, pp.201-218, 2008.

R. Diaconescu, Axiom of choice and complementation, Proceedings of the American Mathematical Society, vol.51, issue.1, pp.176-1781975, 1975.
DOI : 10.1090/S0002-9939-1975-0373893-X

C. Domínguez and &. Rubio, Computing in Coq with Infinite Algebraic Data Structures, 2010.
DOI : 10.1007/978-3-642-14128-7_18

F. Garillot and &. Werner, Simple Types in Type Theory: Deep and Shallow Encodings, Proceedings of the 20th international conference on Theorem proving in higher order logics, pp.368-382, 2007.
DOI : 10.1007/978-3-540-74591-4_27

J. Girard, Locus solum: From the rules of logic to the logic of rules, Mathematical Structures in Computer Science, vol.11, issue.03, pp.301-506, 2001.

G. Gonthier, A computer-checked proof of the four colour theorem, 2004.

G. Gonthier and &. Mahboubi, A Small Scale Reflection Extension for the Coq system, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00258384

M. Gordon, R. Milner, and C. Wadsworth, Edinburgh LCF: A mechanised logic of computation, 1979.
DOI : 10.1007/3-540-09724-4

B. Grégoire and &. Leroy, A compiled implementation of strong reduction, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, pp.235-246, 2002.

B. Grégoire and &. Mahboubi, Proving Equalities in a Commutative Ring Done Right in Coq, Theorem Proving in Higher Order Logics, pp.98-113, 2005.
DOI : 10.1007/11541868_7

B. Grégoire and &. Laurent-théry, A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers, Automated Reasoning, pp.423-437, 2006.
DOI : 10.1007/11814771_36

D. Howe, Higher-Order Abstract Syntax in Isabelle/HOL. Interactive Theorem Proving, pp.481-484, 2010.
DOI : 10.1007/978-3-642-14052-5_33

A. Ofman, Multiplication of manydigital numbers by automatic computers, Doklady Akad. Nauk SSSR, p.85, 1962.

G. Maxwell and K. , Basic concepts of enriched category theory Strategic Computation and Deduction, Theory And Applications Of Categories, issue.10, 1982.

O. Kiselyov, C. Shan, D. P. Friedman, and &. Sabry, Backtracking, interleaving, and terminating monad transformers, ACM SIGPLAN Notices, vol.40, issue.9, p.192, 2005.
DOI : 10.1145/1090189.1086390

F. and W. Lawvere, Adjointness in Foundations. Dialectica, pp.281-296, 1969.

T. Leinster, Higher Operads, Higher Categories, p.305049, 2003.
DOI : 10.1017/CBO9780511525896

S. Lengrand, R. , and J. Mckinna, A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems, Logical Methods in Computer Science, vol.7, issue.1, 2010.
DOI : 10.2168/LMCS-7(1:6)2011
URL : https://hal.archives-ouvertes.fr/hal-01110478

X. Leroy, The Zinc Experiment: An Economical Implementation Of The ML Language, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00070049

S. Mac and L. Moerdijk, Sheaves in geometry and logic: A first introduction to topos theory, 1992.

P. Martin-löf, Intuitionistic type theory, pp.819-828, 1984.

C. Mcbride, The derivative of a regular type is its type of one-hole contexts. Unpublished manuscript, 2001.

C. Muñoz, A calculus of substitutions for incomplete-proof representation in type theory, 1997.

U. Norell, Towards a practical programming language based on dependent type theory, 2007.

C. Okasaki, Purely functional data structures, 1999.
DOI : 10.1017/CBO9780511530104
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.505

J. Penon, Sur les quasi-topos. Cahiers de topologie et géométrie différentielle catégorique, pp.181-218, 1977.

J. Rubio and &. Sergeraert, Constructive homological algebra and applications URL http://map.disi.unige.it/summer_school/pdf/Sergeraert% _MAP_06.pdf [49] Francis Sergeraert, Yvon Siret & Xavier Dousson. The Kenzo program, 2006.

M. Sozeau, Subset coercions in Coq. Types for Proofs and Programs, pp.237-252, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00628869

A. Spiwack, An abstract type for constructing tactics in Coq, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00502500

T. Streicher, Semantical investigations into intensional type theory, 1993.

P. Strub, Coq Modulo Theory, Computer Science Logic, pp.529-543, 2010.
DOI : 10.1007/978-3-642-15205-4_40
URL : https://hal.archives-ouvertes.fr/inria-00497404