B. Beckert, R. Hähnle, and P. H. Schmitt, Verification of Object-Oriented Software: The KeY Approach, LNCS, vol.4334, 2007.
DOI : 10.1007/978-3-540-69061-0

B. Blanchet, Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software, The Essence of Computation: Complexity, Analysis, Transformation. LNCS 2566, pp.85-108, 2002.
DOI : 10.1007/3-540-36377-7_5
URL : https://hal.archives-ouvertes.fr/inria-00528442

S. Robert, W. A. Boyer, and . Jr, Function memoization and unique object representation for ACL2 functions, pp.81-89, 2006.

T. Braibant, J. Jourdan, and D. Monniaux, Supplementary material. url: https

L. Bulwahn, Imperative Functional Programming with Isabelle In: Theorem Proving in Higher Order Logics (TPHOL), LNCS, vol.5170, pp.134-149, 2008.

A. Charguéraud, Characteristic Formulae for the Verification of Imperative Programs, Proceeding of the 16th ACM SIGPLAN International Conference on Functional programming (ICFP), pp.418-430, 2011.

J. Christiansen and F. Huch, A purely functional implementation of ROBDDs in Haskell In: Trends in Functional Programming Trends in Functional Programming, Henrik Nilsson. Intellect, vol.7, pp.55-71, 2006.

S. Conchon and J. Filliâtre, Type-Safe Modular Hash- Consing, In: ACM SIGPLAN Workshop on ML. Portland, 2006.

M. Giorgino and M. Strecker, Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction, LNCS, vol.7436, pp.202-216, 2012.
DOI : 10.1007/978-3-642-32759-9_18

J. Goubault, HimML: Standard ML with Fast Sets and Maps, 5th ACM SIGPLAN Workshop on ML and its Applications, 1994.

J. Goubault, Implementing Functional Languages with Fast Equality, Sets and Maps: an Exercise in Hash Consing, Tech. rep. Bull S.A. Research Center, 1994.

J. Goubault-larrecq, HimML: HimML is a map-oriented ML, 2008.

G. Huet, Constructive Computation Theory, Course notes

N. Davies and J. Bradley, Compositional BDD Construction: A Lazy Algorithm . Tech. rep. CSTR-98-005, 1998.

E. Donald and . Knuth, The Art of Computer Programming Binary decision diagrams, 2011.

G. Melquiond, Floating-point arithmetic in the Coq system, Information and Computation, vol.216, pp.14-23, 2012.
DOI : 10.1016/j.ic.2011.09.005
URL : https://hal.archives-ouvertes.fr/hal-00797913

V. Ortner and N. Schirmer, Verification of BDD Normalization, In: TPHOLs. Lecture Notes in Computer Science, vol.3603, pp.261-277, 2005.
DOI : 10.1007/11541868_17

M. Sozeau, Subset Coercions in Coq, In: TYPES. Lecture Notes in Computer Science, vol.4502, pp.237-252, 2007.
DOI : 10.1007/978-3-540-74464-1_16
URL : https://hal.archives-ouvertes.fr/inria-00628869

V. Vafeiadis, Adjustable References, In: ITP. Lecture Notes in Computer Science, vol.7998, pp.328-337, 2013.
DOI : 10.1007/978-3-642-39634-2_24

N. Kumar, J. Verma, and . Goubault-larrecq, Reflecting BDDs in Coq, p.72797, 2000.

. Kumar-neeraj and . Verma, Reflecting BDDs in Coq, Proc. ASIAN, pp.162-181, 2000.