Author: Georges Gonthier
E-mail:gonthier@microsoft.com
Title: The Four Color Theorem in Coq
Abstract: 
This fall we completed a fully formal proof of the famous Four Color
Theorem, using the Coq proof assistant, thus bringing a 5-year old side
project to a close. In this talk we will review the main obstacles of
this formal proof, and present the main techniques that were used to
overcome them, in particular a general and pervasive use of
computational reflection, and a simple tactic "shell" that very
effectively simplifies proof context management.