BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Graduality and Parametricity - Together again for the first time\,
  for the second time - Philip Wadler\, University of Edinburgh
DTSTART:20230314T140000Z
DTEND:20230314T150000Z
UID:TALK198301@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:Gradual types are essential: they support users of untyped\nla
 nguages to migrate to typed languages\, and users of typed\nlanguages to m
 igrate to more strongly typed languages.  \nThe gradual guarantee (gradual
 ity for short) is the key\nproperty that relates the semantics of less sto
 ngly typed and\nmore strongly typed code.\n\nPolymorphic types are essenti
 al.  They are at the core of\nevery typed functional language\, from ML to
  Caml to Haskell\,\nand are one key ingredient of dependently typed langua
 ges\,\nfrom Coq to Agda to Idris.  Parametricity is the key\nproperty that
  governs the semantics of polymorphic types.\n\nAlas\, graduality and para
 metricity are known to be at\nodds\, as explored in a string of work by Ig
 arashi et al\n(2017)\, New at al (2020)\, and Labrada et al (2022).\n(We s
 teal our title from the second of these.) Here we\npropose a new solution 
 combining ideas from all three.\n\nJoint work with Jeremy Siek and Peter T
 hiemann.
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR