G. Henry and . Baker, Shallow Binding Makes Functional Arrays Fast, ACM SIGPLAN notices, vol.26, pp.1991-145, 1991.

B. Barras and B. Grégoire, On the Role of Type Decorations in the Calculus of Inductive Constructions, CSL, pp.151-166, 2005.
DOI : 10.1007/11538363_12

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development . Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

S. Robert, J. Boyer, and . Strother-moore, Single-Threaded Objects in ACL2, PADL'2001, pp.9-27, 2001.

L. Bulwahn, A. Krauss, F. Haftmann, L. Erkök, and J. Matthews, Imperative Functional Programming with Isabelle/HOL, TPHOLs'08, pp.134-149, 2008.
DOI : 10.1007/978-3-540-74591-4_23
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.176.4954

S. Conchon and J. Filliâtre, A persistent union-find data structure, Proceedings of the 2007 workshop on Workshop on ML , ML '07, pp.37-46, 2007.
DOI : 10.1145/1292535.1292541

A. Darbari, B. Fischer, and J. Marques-silva, Formalizing a SAT Proof Checker in Coq. First Coq Workshop, published as technical report tum-i0919 of, 2009.

G. Gonthier, Formal Proof ? The Four-Color Theorem, Notices of the AMS, vol.55, issue.11, 2008.

B. Grégoire and X. Leroy, A compiled implementation of strong reduction, ICFP, pp.235-246, 2002.

D. Kroening and O. Strichman, Decision Procedures, An Algorithmic Point of View. Texts in Theoretical Computer Science, 2008.

X. Leroy, The ZINC experiment: an economical implementation of the ML language, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00070049

X. Leroy, Objective Caml Available at http://ocaml.inria.fr, 1997.

C. Okasaki, Purely Functional Data Structures, 1998.
DOI : 10.1017/CBO9780511530104
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.505

N. Shankar, Static Analysis for Safe Destructive Updates in a Functional Language, LOPSTR, volume 2372 of LNCS, pp.1-24, 2001.
DOI : 10.1007/3-540-45607-4_1

W. Swierstra, A Hoare Logic for the State Monad, TPHOLs'09, pp.440-451, 2009.
DOI : 10.1007/978-3-540-74591-4_23

L. Théry, Proof Pearl: Revisiting the Mini-rubik in Coq, TPHOLS'08, pp.310-319, 2008.
DOI : 10.1007/s10009-005-0191-z

P. Wadler, Monads for Functional Programming, Advanced Functional Programming, pp.24-52, 1995.

T. Weber and H. Amjad, Efficiently checking propositional refutations in HOL theorem provers, Journal of Applied Logic, vol.7, issue.1, pp.26-40, 2009.
DOI : 10.1016/j.jal.2007.07.003