2019/07/25 by Lau Skorstengaard, Skorstengaard, Lau
Computer Science · #FOS: Computer and information sciences #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL) #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.1907.11133
openalex publication_date 2019/07/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.