Events

Back to Listing

NCSA staff who would like to submit an item for the calendar can email newsdesk@ncsa.illinois.edu.

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

Event Type
Lecture
Sponsor
Center for Advanced Study
Location
Knight Auditorium, Spurlock Museum; 600 South Gregory; Urbana IL
Date
Nov 3, 2017   4:00 pm  
Speaker
Andrew W. Appel, Eugene Higgins Professor of Computer Science, Princeton University
Cost
Free and Open to the Public
E-Mail
cas@cas.illinois.edu
Phone
217-333-6729
Views
30
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