Fundur með erindi

Georges Gonthier of Microsoft Research will give a talk at Reykjavik University, room V.1.01, on Thursday May 26. The meeting will start with refreshments at 4:30 pm and the talk will start at 5 pm. The title is: Verifying the Four Colour Theorem.

This is a joint event with ICE-TCS, the Icelandic Centre for Excellence in Computer Science at Reykjavik University.

Abstract: The 150-year-old Four Colour Theorem is the first famous result with a proof that requires large computer calculations. Such proofs are still controversial: It is thought that computer programs cannot be reviewed with mathematical rigor. To overturn this belief, we have created a fully computer-checked proof of the Four Colour Theorem. Using the Coq proof assistant, we wrote an extended program that specifies both the calculations and their mathematical justification. Only the interface of the program – the statement of the theorem – needs to be reviewed. The rest (99.8%) is self-checking: Coq verifies that it strictly follows the rules of logic. Thus, our proof is more rigorous than a traditional one.

Biography: Georges Gonthier received his Doctorate in 1988 from Université Paris XI for work on the Esterel reactive programming language. After two years at AT&T Bell Labs, he returned to France at INRIA in 1990. His work includes the optimal computation of functional programs, the formal verification of a concurrent memory management algorithm, and concurrency analysis of the Ariane 5 flight software. Dr Gonthier joined Microsoft Research Cambridge in 2003, where he completed the first fully computer-checked proof of the famous Four Colour Theorem.

Update: The talk was recorded and is available at http://www.ru.is/kennarar/luca/TALKS/Gonthier.avi