General Events

Back to Listing

CAS Special Presentation: Four Color Theorem Festival--Graph Coloring and Machine Proofs in Computer Science, 1977-2017

Event Type
Center for Advanced Study
Knight Auditorium, Spurlock Museum; 600 South Gregory; Urbana IL
Nov 3, 2017   4:00 pm  
Andrew W. Appel, Eugene Higgins Professor of Computer Science, Princeton University
Free and Open to the Public
Originating Calendar
Center for Advanced Study

The Four Color Theorem of Kenneth Appel and Wolfgang Haken (1976) was proved and checked with the assistance of computer programs, though much of the proof was written (and refereed) only by humans. Contemporaneously, Edinburgh LCF (Logic for Computable Functions) was developed by Robin Milner-a system for proofs written by humans (with computer assistance) but completely checked by computer; with particular application to proofs about computer programs. These two developments, and their convergence, have had significant impact on computer science, and my own research career: graph-coloring algorithms for register allocation in compilers, functional programming languages, fully machine-checked proofs of mathematical theorems, fully machine-checked proofs of software systems. One result at the intersection of all these is a machine-checked proof of correctness of a program that does register allocation by graph-coloring, using an algorithm related to one used in every four-color proof (and attempted proof) since 1879.

Reception follows in the Ballroom, Alice Campbell Alumni Center, 601 S. Lincoln, Urbana

link for robots only