Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, Coq'Art :the Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

E. Chailloux, P. Manoury, and B. Pagano, Déveleoppement d'applications avec Objective Caml, 2000.
DOI : 10.3166/tsi.24.1055-1080

R. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer et al., Implementing mathematics with the Nuprl proof development system, 1986.

L. Damas and R. Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '82, pp.207-212, 1982.
DOI : 10.1145/582153.582176
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.645.5233

J. Girard, Y. Lafont, and P. Taylor, Proofs and types, 1989.

J. C. Michael, T. F. Gordon, and . Melham, Introduction to HOL : a theorem proving environment for higher-order logic, 1993.

F. Kamareddine, T. Laan, and R. Nederpelt, A Modern Perspective on Type Theory From its Origins Until Today, 2004.

J. Krivine, Lambda Calcul, types et modèles, 1990.
DOI : 10.1051/ita/1991250100671
URL : http://archive.numdam.org/article/ITA_1991__25_1_67_0.pdf

C. Lawrence and . Paulson, Logic and computation, Interactive proof with Cambridge LCF, 1987.

C. Lawrence and . Paulson, ML for the working programmer, 1991.

C. Lawrence, T. Paulson, and . Nipkow, Isabelle : a generic theorem prover, Lecture Notes in Computer Science, vol.828, 1994.