M. Armand, Extending Coq with Imperative Features and Its Application to SAT Verification, Proc. ITP. LNCS, vol.6172, pp.83-98, 2010.
DOI : 10.1007/978-3-642-14052-5_8
URL : https://hal.archives-ouvertes.fr/inria-00502496

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

E. Donald and . Knuth, The Art of Computer Programming Binary decision diagrams, pp.978-0201038040, 2011.

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

. Kumar-neeraj and . Verma, Reflecting BDDs in Coq, Proc. ASIAN. LNCS. Springer, vol.isbn, pp.162-181, 1961.