BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/811
DTSTAMP:20230914T125939Z
SUMMARY:Logical Relations
DESCRIPTION:Speaker: Ankit K. (School of Technology and Computer Science\nT
 ata Institute of Fundamental Research\nHomi Bhabha Road\nNavy Nagar\nMumba
 i 400005)\n\nAbstract: \nLogical relations are proof techniques that can b
 e used to prove properties about languages like normalization\, type safet
 y\, program equivalence and are closed under elimination. Hence they can b
 e used to prove properties which are not closed under elimination\, such 
 as termination in the Simply Typed Lambda Calculus (STLC).\n\nThe term ``l
 ogical relations” was first introduced by Gordon Plotkin in his memorand
 um ``Lambda- definability and logical relations" in 1973.\n\nThe analogy 
 between types and logics\, also called the Curry Howard isomorphism allows
  us to view types as logical formulae (times as conjunction\, → as imp
 lication etc..).\n\nLogical Relations are named so because\n\n(i) they are
  relations\n\n(ii) which treat type constructors as logical connectives\, 
 hence ``Logical”.\n\nThe talk will start with the simply typed lambda c
 alculus (STLC)\, introduction of types and typing rules\, and then the int
 roduction and usage of logical relations to prove properties about the STL
 C and its variants.\n
URL:https://www.tcs.tifr.res.in/web/events/811
DTSTART;TZID=Asia/Kolkata:20170929T160000
DTEND;TZID=Asia/Kolkata:20170929T170000
LOCATION:A-201 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR