Tata Institute of Fundamental Research
Logical Relations
STCS Student Seminar
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)
Abstract:
Logical relations are proof techniques that can be used to prove properties about languages like normalization, type safety, program equivalence and are closed under elimination. Hence they can be used to prove properties which are not closed under elimination, such as termination in the Simply Typed Lambda Calculus (STLC).
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.
| 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)
Abstract:
Logical relations are proof techniques that can be used to prove properties about languages like normalization, type safety, program equivalence and are closed under elimination. Hence they can be used to prove properties which are not closed under elimination, such as termination in the Simply Typed Lambda Calculus (STLC).
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.
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.