Four-colored county map of Illinois bounded by rectangular outline of text

Presentation: “Graph Coloring and Machine Proofs in Computer Science, 1977-2017” by Andrew W. Appel

Part of the Four Color Fest

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.

This event is a special presentation by the Center for Advanced Study and is part of the University of Illinois Department of Mathematics Four Color Festival which celebrates the 40th anniversary of the proof of the Four Color Theorem. The festival is a part of the 2017 sesquicentennial celebration of the founding of the University of Illinois.

Additional information about the Four Color Fest can be found on their website (external link)

Add Event to CalendarAdd to Calendar

Contact

For further information, visit the Center for Advanced Study (external link) or call (217) 333-6729.

To request disability-related accommodations for this event, please contact Brian Cudiamat at or (217) 244-5586.