Universal Types and Relational Substitutions

This meeting is a very beginner-friendly refresher on the interplay between parametricity and logical relations to prove program equivalence. Upon request, the session will be hosted as a hybrid event.

We will meet again in autumn. Enjoy your summer!

Material

The material to be read before the meeting is chapter 4 from Skorstengaard, L.: An Introduction to Logical Relations, https://arxiv.org/abs/1907.11133. Try to solve the exercise at the end of the chapter!

Abstract (of the entire tutorial)

Logical relations (LR) have been around for many years, and today they are used in many formal results. However, it can be difficult to LR beginners to find a good place to start to learn. Papers often use highly specialized LRs that use the latest advances of the technique which makes it impossible to make a proper presentation within the page limit.

This note is a good starting point for beginners that want to learn about LRs. Almost no prerequisite knowledge is assumed, and the note starts from the very basics. The note covers the following: LRs for proving normalization and type safety of simply typed lambda calculus, relational substitutions for reasoning about universal and existential types, step-indexing for reasoning about recursive types, and worlds for reasoning about references.

Before joining

Please make sure to be aware of the PLUSLE format before joining.