# An Introduction to Logical Relations

## TL;DR

This paper provides an accessible introduction to logical relations, covering fundamental concepts and applications such as normalization, type safety, and reasoning about complex types, aimed at beginners with minimal prerequisites.

## Contribution

It offers a beginner-friendly overview of logical relations, explaining core ideas and techniques without assuming prior specialized knowledge.

## Key findings

- Logical relations can be used to prove normalization and type safety.
- Relational substitutions help reason about universal and existential types.
- Step-indexing and worlds are effective tools for reasoning about recursive types and references.

## Abstract

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.