BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:TALK CANCELLED: Explicit Weakening (A Functional Pearl) - Professo
 r Philip Wadler - Professor of Theoretical Computer Science\, Laboratory f
 or Foundations of Computer Science\, School of Informatics\, University of
  Edinburgh
DTSTART:20230315T150500Z
DTEND:20230315T155500Z
UID:TALK196933@talks.cam.ac.uk
CONTACT:Ben Karniely
DESCRIPTION:TALK CANCELLED\n\nWe present a novel formulation of substituti
 on\, inspired by the explicit substitutions of Abadi\, Cardelli\, Curien\,
  and Levy (1991). In their formulation\, substitutions are constructed wit
 h four operations and substitution is an explicit operator on terms.  In o
 ur formulation\, substitutions are constructed with three operations and w
 eakening is an explicit operator on terms\, while substitution becomes a m
 eta operation.  The advantage of our formulation is that facts about subst
 itution that previously required tens or hundreds of lines justify in a pr
 oof assistant now follow immediately---they can be justified by writing th
 e four letters "refl".\n\nA paper has been written as an executable litera
 te Agda script\, and source of the paper is available as an artifact.\n\nJ
 oint work with Jeremy Siek and Peter Thiemann.\n\nBio:\n\nPhilip Wadler li
 kes to introduce theory into practice\, and practice into theory. An examp
 le of theory into practice: GJ\, the basis for Java with generics\, derive
 s from quantifiers in second-order logic. An example of practice into theo
 ry: Featherweight Java specifies the core of Java in less than one page of
  rules. He is a principal designer of the Haskell programming language\, c
 ontributing to its two main innovations\, type classes and monads. The You
 Tube video of his Strange Loop talk Propositions as Types has over 75\,000
  views.\n\nPhilip Wadler is Professor of Theoretical Computer Science at t
 he University of Edinburgh and Senior Research Fellow at IOHK. He is an AC
 M Fellow\, a Fellow of the Royal Society of Edinburgh\, and editor-in-chie
 f of Proceedings of the ACM for Programming Languages. He is past chair of
  ACM SIGPLAN\, past holder of a Royal Society-Wolfson Research Merit Fello
 wship\, winner of the SIGPLAN Distinguished Service Award\, and a winner o
 f the POPL Most Influential Paper Award. Previously\, he worked or studied
  at Stanford\, Xerox Parc\, CMU\, Oxford\, Chalmers\, Glasgow\, Bell Labs\
 , and Avaya Labs\, and visited as a guest professor in Copenhagen\, Sydney
 \, and Paris. He has an h-index of over 70 with more than 25\,000 citation
 s to his work\, according to Google Scholar. He contributed to the designs
  of Haskell\, Java\, and XQuery\, and is co-author of Introduction to Func
 tional Programming (Prentice Hall\, 1988)\, XQuery from the Experts (Addis
 on Wesley\, 2004)\, Generics and Collections in Java (O'Reilly\, 2006)\, a
 nd Programming Language Foundations in Agda (2018). He has delivered invit
 ed talks in locations ranging from Aizu to Zurich.\n\n\nLink to join virtu
 ally: https://zoom.us/j/98901725392?pwd=UWNVZVFTcVQxL2JkS0V1WVBoelBuUT09\n
 \nThis talk is being recorded.
LOCATION:Lecture Theatre 1\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR