J. Abrial, D. Cansell, and D. Méry, Formal Derivation of Spanning Trees Algorithms, ZB 2003, pp.457-476, 2003.
DOI : 10.1007/3-540-44880-2_27
URL : https://hal.archives-ouvertes.fr/inria-00099793

A. W. Appel, Modern Compiler Implementation in ML, 1998.
DOI : 10.1017/CBO9780511811449

A. W. Appel and L. George, Optimal spilling for CISC machines with few registers, 2001.

K. Appel and W. Haken, Every planar map is four colorable, Bulletin of the American Mathematical Society, vol.82, issue.5, pp.711-712, 1976.
DOI : 10.1090/S0002-9904-1976-14122-5

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

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.
URL : https://hal.archives-ouvertes.fr/hal-00344237

S. Blazy, Z. Dargaye, and X. Leroy, Formal Verification of a C Compiler Front-End, FM 2006, pp.460-475, 2006.
DOI : 10.1007/11813040_31
URL : https://hal.archives-ouvertes.fr/inria-00106401

P. Briggs, K. D. Cooper, and L. Torczon, Improvements to graph coloring register allocation, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.428-455, 1994.
DOI : 10.1145/177492.177575

G. J. Chaitin, M. A. Auslander, A. K. Chandra, J. Cocke, M. E. Hopkins et al., Register allocation via coloring, Computer Languages, vol.6, issue.1, pp.47-57, 1981.
DOI : 10.1016/0096-0551(81)90048-5

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, HUG 1994, pp.144-157, 1994.

. Coq, The coq proof assistant
URL : https://hal.archives-ouvertes.fr/inria-00069919

L. George and A. W. Appel, Iterated register coalescing, ACM Transactions on Programming Languages and Systems, vol.18, issue.3, pp.300-324, 1996.
DOI : 10.1145/229542.229546

G. Gonthier, Formal proof ? the four-color theorem, Notices of the American Mathematical Society, vol.55, issue.11, pp.1382-1393, 2008.

S. Hack and G. Goos, Copy coalescing by graph recoloring, 2008.

A. B. Kempe, On the Geographical Problem of the Four Colours, American Journal of Mathematics, vol.2, issue.3, pp.193-200, 1879.
DOI : 10.2307/2369235

X. Leroy, Formal certification of a compiler back-end or: Programming a compiler with a proof assistant, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

J. S. Moore and Q. Zhang, Proof Pearl: Dijkstra???s Shortest Path Algorithm Verified with ACL2, TPHOLs 2005, pp.373-384, 2005.
DOI : 10.1007/11541868_24

G. C. Necula, Translation validation for an optimizing compiler, ACM SIGPLAN Notices, vol.35, issue.5, pp.83-94, 2000.
DOI : 10.1145/358438.349314

A. Pnueli, M. Siegel, and E. Singerman, Translation validation, TACAS 1998, pp.151-166, 1998.
DOI : 10.1007/BFb0054170

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 1998, pp.479-496, 1998.
DOI : 10.1007/BFb0055153