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