An Introduction to Logical Relations
An Introduction to Logical Relations
复制标题
逻辑关系简介
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Lau Skorstengaard
中科院分区：
文献类型：
--
作者：
Lau Skorstengaard
逻辑关系（LR）已经存在了很多年，如今它们被用于许多正式结果。但是，很难从初学者那里找到一个开始学习的好地方。论文通常使用高度专业化的LRS来使用该技术的最新进展，这使得无法在页面限制内进行适当的演示文稿。
对于想了解LRS的初学者来说，此注释是一个很好的起点。几乎没有假定的先决条件知识，便条始于基本知识。该说明涵盖以下内容：用于证明简单键入lambda微积分的标准化和类型安全性的LRS，用于推理通用类型和存在类型的关系的关系替换，用于递归类型的推理的阶梯索引以及有关参考推理的世界。
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.