Four Color Fest--Graph Coloring and Machine Proofs in Computer Science, 1977-2017

Friday, November 3rd, 2017
Andrew W. Appel

Knight Auditorium, Spurlock Museum

600 South Gregory


Event Description

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


Andrew W. Appel

Eugene Higgins Professor of Computer Science, Princeton University