一句话：提出证明相关逻辑关系，为含递归的名字生成语言给出直接风格语义模型，并解决动态分配单子失效问题。
Pitts 与 Stark 的 ν-演算是研究高阶语言中名字生成与上下文等价问题的典型全语言。现有模型多用函子范畴或名义集合，并以动态分配单子建模新名分配；但加入递归后，若从（名义）集合转向（名义）域，直接风格的分配单子构造不再成立。此前用分配与续延结合的单子回避该问题，却牺牲了抽象性。本文提出证明相关逻辑关系框架，其中逻辑关系还包含证明对象，用以见证程序语义对应物之间的等价。作者据此为带递归的 ν-演算类语言构造了直接风格模型，为旧问题提供新解法，并给出该框架的易读入门。
Pitts and Stark's $\nu$-calculus is a paradigmatic total language for studying the problem of contextual equivalence in higher-order languages with name generation. Models for the $\nu$-calculus that validate basic equivalences concerning names may be constructed using functor categories or nominal sets, with a dynamic allocation monad used to model computations that may allocate fresh names. If recursion is added to the language and one attempts to adapt the models from (nominal) sets to (nominal) domains, however, the direct-style construction of the allocation monad no longer works. This issue has previously been addressed by using a monad that combines dynamic allocation with continuations, at some cost to abstraction. This paper presents a direct-style model of a $\nu$-calculus-like language with recursion using the novel framework of proof-relevant logical relations, in which logical relations also contain objects (or proofs) demonstrating the equivalence of (the semantic counterparts of) programs. Apart from providing a fresh solution to an old problem, this work provides an accessible setting in which to introduce the use of proof-relevant logical relations, free of the additional complexities associated with their use for more sophisticated languages.
@article{paperbot416,
title = {Proof-Relevant Logical Relations for Name Generation},
author = {Nick Benton and Martin Hofmann and Vivek Nigam},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 1},
year = {2018},
doi = {10.23638/lmcs-14(1:25)2018}
}