BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Bidirectional typing is not just an implementation technique - Mev
 en Lennon-Bertrand\, University of Cambridge
DTSTART:20230203T140000Z
DTEND:20230203T150000Z
UID:TALK195478@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:In 2000\, Pierce and Turner introduced a new technique to perf
 orm type inference for ML-like languages\, whose main idea was to carefull
 y understand the local flow of information in typing rules. This technique
 \, which came to be referred to as bidirectional typing\, did not come out
  of a void: similar ideas had appeared independently in other contexts. In
  particular\, bidirectional typing has been a part of the folklore of depe
 ndently typed languages implementers since the dawn of time.\n\nBut even i
 n that context where it has a long history\, bidirectional typing was miss
 ing an understanding that would detach from implementations to focus on th
 e type-theoretic structure. Fortunately\, such a type-theoretic bidirectio
 nal structure turns out to be a very interesting tool when studying (depen
 dent) type systems.\n\nIn my talk\, I will try and give some of my underst
 anding of bidirectional typing\, how it is both rooted in type-checker imp
 lementations but is more than just this\, and how it can be used to make t
 he infamously painful meta-theory of dependent type systems a bit less pai
 nful.
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR