BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Isaac Newton Institute Seminar Series
SUMMARY:Interpreters for Free - Philip Wadler (University 
 of Edinburgh)
DTSTART;TZID=Europe/London:20220708T133000
DTEND;TZID=Europe/London:20220708T143000
UID:TALK175793AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/175793
DESCRIPTION:In a proof assistant based on intuitionistic logic
 \, a standard proof of type soundness automaticall
 y yields an interpreter for the corresponding lang
 uage. This fact is obvious in retrospect\, but the
 re is evidence it was not obvious in prospect. The
  talk describes applications in the textbook Progr
 amming Language Foundations in Agda and to the Car
 dano blockchain. In connection with the latter\, w
 e explain why and how Reynolds's and Girard's Syst
 em F\, from the 1970s\, is used to encode smart co
 ntracts that manipulate billions of dollars worth 
 of assets: if you want a system that will still be
  running in fifty years\, use one that is fifty ye
 ars old!
LOCATION:Seminar Room 1\, Newton Institute
CONTACT:
END:VEVENT
END:VCALENDAR