Georges Gonthier

Georges Gonthier
PRINCIPAL RESEARCHER
.

Georges Gonthier's research interests include programming language design and semantics, concurrency theory and its application to security, and methods and tools for the formal verification of computer programs. One of his achievements on the latter subject is a fully checked formal proof of the famous Four Colour Theorem, using the Coq proof assistant developed at INRIA, the French Institut National de Recherche en Informatique et Automatique (this was work in collaboration with Benjamin Werner of INRIA).

Mathematically inclined readers may consult a paper describing the mathematics of the formalization. Users of the Coq system, or brave souls wishing to delve into the actual Coq Proof of the Four Color Theorem, might also be interested in description of the notations and the proof command language that were used to write the proof.