BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//jEvents 2.0 for Joomla//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
BEGIN:VTIMEZONE
TZID:America/New_York
BEGIN:STANDARD
DTSTART:20191103T010000
RDATE:20200308T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20201101T010000
RDATE:20210314T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20211107T010000
RDATE:20220313T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20221106T010000
RDATE:20230312T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20231105T010000
RDATE:20240310T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20241103T010000
RDATE:20250309T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20251102T010000
RDATE:20260308T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20261101T010000
RDATE:20270314T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20271107T010000
RDATE:20280312T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20281105T010000
RDATE:20290311T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:DAYLIGHT
DTSTART:20190402T170000
RDATE:20191103T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20200308T030000
RDATE:20201101T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20210314T030000
RDATE:20211107T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20220313T030000
RDATE:20221106T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20230312T030000
RDATE:20231105T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20240310T030000
RDATE:20241103T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20250309T030000
RDATE:20251102T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20260308T030000
RDATE:20261101T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20270314T030000
RDATE:20271107T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20280312T030000
RDATE:20281105T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:3bd5bf3967f529cfddde07ed7d91b64e
CATEGORIES:Experimental Mathematics Seminar
CREATED:20200330T090504
SUMMARY:Graph coloring and machine proofs in computer science, 1977-2017 
LOCATION:Join Zoom Meeting Meeting ID: 341 312 077.
DESCRIPTION:Abstract: The Four Color Theorem of Kenneth Appel and Wolfgang Haken (1976)
  was proved and checked with the assistance of computer programs, though mu
 ch of the proof was written (and refereed) only by humans. Contemporaneousl
 y, Edinburgh LCF (Logic for Computable Functions) was developed by Robin Mi
 lner--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 progra
 mming languages, fully machine-checked proofs of mathematical theorems, ful
 ly machine-checked proofs of software systems. One result at the intersecti
 on 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.\nJoin 
 Zoom Meeting (https://princeton.zoom.us/j/341312077) Meeting ID: 341 312 07
 7.\n
X-ALT-DESC;FMTTYPE=text/html:<p><em style="color: #000000; font-family: Times; font-size: medium; font-w
 eight: 400; letter-spacing: normal; orphans: 2; text-align: start; text-ind
 ent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacin
 g: 0px;">Abstract</em>: The Four Color Theorem of Kenneth Appel and Wolfgan
 g Haken (1976) was proved and checked with the assistance of computer progr
 ams, though much of the proof was written (and refereed) only by humans. Co
 ntemporaneously, Edinburgh LCF (Logic for Computable Functions) was develop
 ed by Robin Milner--a system for proofs written by humans (with computer as
 sistance) but completely checked by computer; with particular application t
 o proofs about computer programs. These two developments, and their converg
 ence, have had significant impact on computer science, and my own research 
 career: graph-coloring algorithms for register allocation in compilers, fun
 ctional 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 algorit
 hm related to one used in every four-color proof (and attempted proof) sinc
 e 1879.</p><p style="color: #000000; font-family: Times; font-size: medium;
  font-weight: 400; letter-spacing: normal; orphans: 2; text-align: start; t
 ext-indent: 0px; text-transform: none; white-space: normal; widows: 2; word
 -spacing: 0px;"><a href="https://princeton.zoom.us/j/341312077">Join Zoom M
 eeting</a>&nbsp;Meeting ID: 341 312 077.</p>
CONTACT:Andrew Appel, Princeton University. 
DTSTAMP:20260929T123759
DTSTART;TZID=America/New_York:20200402T170000
DTEND;TZID=America/New_York:20200402T180000
SEQUENCE:0
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR