Speaker: |
Ankit K. (School of Technology and Computer Science Tata Institute of Fundamental Research Homi Bhabha Road Navy Nagar Mumbai 400005) |

Organiser: |
Prerona Chatterjee |

Date: |
Friday, 29 Sep 2017, 16:00 to 17:00 |

Venue: |
A-201 (STCS Seminar Room) |

(Scan to add to calendar)

The term ``logical relations” was first introduced by Gordon Plotkin in his memorandum ``Lambda- definability and logical relations" in 1973.

The analogy between types and logics, also called the Curry Howard isomorphism allows us to view types as logical formulae (times as conjunction, → as implication etc..).

Logical Relations are named so because

(i) they are relations

(ii) which treat type constructors as logical connectives, hence ``Logical”.

The talk will start with the simply typed lambda calculus (STLC), introduction of types and typing rules, and then the introduction and usage of logical relations to prove properties about the STLC and its variants.