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:<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:20260929T152251
DTSTART;TZID=America/New_York:20200402T170000
DTEND;TZID=America/New_York:20200402T180000
SEQUENCE:0
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR