J. M. Aransay, Razonamiento mecanizado enálgebraenálgebra homológica, 2006.

M. Artin, A. Grothendieck, J. L. Verdier, and . Univers, Séminaire de Géométrie Algébrique du Bois Marie -1963-64 -Théorie des topos et cohomologié etale des schémas -(SGA 4, pp.185-217

E. Bishop, Foundations of Constructive Analysis, 1967.

N. G. De-bruijn, Telescopic mappings in typed lambda calculus, Information and Computation, vol.91, issue.2, pp.189-204, 1991.
DOI : 10.1016/0890-5401(91)90066-B

M. Barakat and D. Robertz, homalg: First steps to an abstract package for homological algebra, Proceedings of the X meeting on computational algebra and its applications Sevilla (Spain), pp.29-32, 2006.

. Th and . Coquand, Metamathematical investigations of a calculus of constructions, 1989.

B. Gregoire and X. Leroy, A Compiled Implementation of Strong Reduction, International Conference on Functional Programming, 2002.
URL : https://hal.archives-ouvertes.fr/hal-01499941

G. Huet and A. Saibi, Constructive category theory. Proof, language, and interaction, Found. Comput. Ser, pp.239-275, 2000.

P. Landin, The Mechanical Evaluation of Expressions, The Computer Journal, vol.6, issue.4, pp.308-320, 1964.
DOI : 10.1093/comjnl/6.4.308

P. Martin-löf, An intuitionistic theory of types. in Twenty-five years of constructive type theory, pp.127-172, 1995.

P. Mellì-es and B. Werner, A Generic Normalization Proof for Pure Type Systems, TYPES'96, C. Paulin-Mohring, E. Gimenez (rd.), LNCS, 1997.

A. Miquel and B. Werner, The Not So Simple Proof-Irrelevant Model of CC, 2003.
DOI : 10.1007/3-540-39185-1_14

R. Mines, F. Richman, and W. Ruitenburg, A Course in Constructive Algebra, 1988.
DOI : 10.1007/978-1-4419-8640-5

J. Rubio and F. Sergereart, Constructive Homological Algebra and Applications, Genove Summer School. Available at, 2006.

A. Spiwack, Ajouter des entiers machinè a Coq