Logical Relations

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 ``ogical”.

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.