BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Interpreters for Free - Philip Wadler (University of Edinburgh)
DTSTART:20220708T123000Z
DTEND:20220708T133000Z
UID:TALK175793@talks.cam.ac.uk
DESCRIPTION:In a proof assistant based on intuitionistic logic\, a standar
 d proof of type soundness automatically yields an interpreter for the corr
 esponding language. This fact is obvious in retrospect\, but there is evid
 ence it was not obvious in prospect. The talk describes applications in th
 e textbook Programming Language Foundations in Agda and to the Cardano blo
 ckchain. In connection with the latter\, we explain why and how Reynolds's
  and Girard's System F\, from the 1970s\, is used to encode smart contract
 s that manipulate billions of dollars worth of assets: if you want a syste
 m that will still be running in fifty years\, use one that is fifty years 
 old!
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR