E. Alkassar, S. Böhme, K. Mehlhorn, and C. Rizkallah, A Framework for the Verification of Certifying Computations, Journal of Automated Reasoning, vol.5, issue.2, pp.241-273, 2014.
DOI : 10.1007/s10817-013-9289-2

G. Bauer and T. Nipkow, The 5 Colour Theorem in Isabelle/Isar, TPHOLs, pp.67-82, 2002.
DOI : 10.1007/3-540-45685-6_6

S. Blazy, B. Robillard, and A. W. Appel, Formal Verification of Coalescing Graph-Coloring Register Allocation, Programming Languages and Systems, 19th European Symposium on Programming Proceedings, pp.145-164, 2010.
DOI : 10.1007/978-3-642-11957-6_9
URL : https://hal.archives-ouvertes.fr/inria-00477689

S. Blazy, B. Robillard, and E. Soutif, Vérification formelle d'un algorithme d'allocation de registres par coloration de graphe, JFLA'08 Journées Francophones des Langages Applicatifs, pp.31-46, 2008.

M. Carlier, C. Dubois, and A. Gotlieb, A Certified Constraint Solver over Finite Domains, Formal Methods (FM), pp.116-131
DOI : 10.1007/978-3-642-32759-9_12
URL : https://hal.archives-ouvertes.fr/hal-01126135

J. Chen, Dijkstra's shortest path algorithm, Journal of Formalized Mathematics, vol.15, 2003.

C. Chou, A formal theory of undirected graphs in higher-order logic, Workshop on Higher Order Logic Theorem Proving and Its Applications, 1994.

C. Dehlinger and J. Dufourd, Formalizing generalized maps in Coq, Theoretical Computer Science, vol.323, issue.1-3, pp.351-397, 2004.
DOI : 10.1016/j.tcs.2004.05.003

J. Dufourd, An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps, Journal of Automated Reasoning, vol.47, issue.5, pp.19-51, 2009.
DOI : 10.1007/s10817-009-9117-x

J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards Section B Mathematics and Mathematical Physics, vol.69, issue.1 and 2, pp.125-130, 1965.
DOI : 10.6028/jres.069B.013

J. Filliâtre and P. Letouzey, Functors for Proofs and Programs, ESOP, pp.370-384, 2004.
DOI : 10.1007/978-3-540-24725-8_26

J. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, Computer Aided Verification, 19th International Conference Proceedings, pp.173-177, 2007.
DOI : 10.1007/978-3-540-73368-3_21

G. Gonthier, Formal proof ? the four-color theorem. Notices of the, pp.1382-1393, 2008.

P. Letouzey, Extraction in Coq: An Overview, Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, 2008.
DOI : 10.1007/978-3-540-69407-6_39
URL : https://hal.archives-ouvertes.fr/hal-00338973

K. Mehlhorn, S. Näher, and C. Uhrig, The LEDA platform for combinatorial and geometric computing, Automata, Languages and Programming, pp.7-16, 1997.
DOI : 10.1007/3-540-63165-8_161

J. , S. Moore, and Q. Zhang, Proof pearl : Dijkstra's shortest path algorithm verified with ACL2, TPHOLs, pp.373-384, 2005.

T. Nipkow, Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism, Interactive Theorem Proving, pp.281-296, 2011.
DOI : 10.1007/s10472-009-9168-z

L. Noschinski, A Graph Library for Isabelle, Mathematics in Computer Science, vol.6, issue.3, 2014.
DOI : 10.1007/s11786-014-0183-z

J. Régin, A filtering algorithm for constraints of difference in csps, 12th National Conference on Artificial Intelligence (AAAI'94), pp.362-367, 1994.

M. Yamamoto, S. Nishizaki, M. Hagiya, and Y. Toda, Formalization of planar graphs, Workshop on Higher Order Logic Theorem Proving and Its Applications, pp.369-384, 1995.
DOI : 10.1007/3-540-60275-5_77

M. Yamamoto, K. Takahashi, M. Hagiya, S. Nishizaki, and T. Tamai, Formalization of graph search algorithms and its applications, TPHOLs, pp.479-496, 1998.
DOI : 10.1007/BFb0055153