Razonamiento mecanizado enálgebraenálgebra homológica, 2006. ,
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 ,
Foundations of Constructive Analysis, 1967. ,
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
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. ,
Metamathematical investigations of a calculus of constructions, 1989. ,
A Compiled Implementation of Strong Reduction, International Conference on Functional Programming, 2002. ,
URL : https://hal.archives-ouvertes.fr/hal-01499941
Constructive category theory. Proof, language, and interaction, Found. Comput. Ser, pp.239-275, 2000. ,
The Mechanical Evaluation of Expressions, The Computer Journal, vol.6, issue.4, pp.308-320, 1964. ,
DOI : 10.1093/comjnl/6.4.308
An intuitionistic theory of types. in Twenty-five years of constructive type theory, pp.127-172, 1995. ,
A Generic Normalization Proof for Pure Type Systems, TYPES'96, C. Paulin-Mohring, E. Gimenez (rd.), LNCS, 1997. ,
The Not So Simple Proof-Irrelevant Model of CC, 2003. ,
DOI : 10.1007/3-540-39185-1_14
A Course in Constructive Algebra, 1988. ,
DOI : 10.1007/978-1-4419-8640-5
Constructive Homological Algebra and Applications, Genove Summer School. Available at, 2006. ,
Ajouter des entiers machinè a Coq ,