一句话：提出用Kripke式逻辑关系证明强规范化的基准，比较Beluga、Coq、Agda等证明助手对机械化元理论的支持。
本文提出一组新的基准问题，用于机械化编程语言元理论并比较、推动证明助手的发展。重点是以逻辑关系为核心的证明，选取带简单类型的演算的强规范化作为基准，并用 Kripke 式逻辑关系给出证明。作者采用现代视角，将逻辑关系建立在良类型项上，并在 Beluga、Coq 和 Agda 等依赖类型证明环境中进行机械化。特别地，论文讨论 Beluga 对高阶抽象语法编码的支持，并与其他通用证明助手的开发策略对比，总结其中的经验教训。最终目标是推动社区讨论证明环境需要哪些支持，才能让机械化元理论广泛可用，并共同设计未来基准。
Abstract We propose a new collection of benchmark problems in mechanizing the metatheory of programming languages, in order to compare and push the state of the art of proof assistants. In particular, we focus on proofs using logical relations (LRs) and propose establishing strong normalization of a simply typed calculus with a proof by Kripke-style LRs as a benchmark. We give a modern view of this well-understood problem by formulating our LR on well-typed terms. Using this case study, we share some of the lessons learned tackling this problem in different dependently typed proof environments. In particular, we consider the mechanization in Beluga, a proof environment that supports higher-order abstract syntax encodings and contrast it to the development and strategies used in general-purpose proof assistants such as Coq and Agda. The goal of this paper is to engage the community in discussions on what support in proof environments is needed to truly bring mechanized metatheory to the masses and engage said community in the crafting of future benchmarks.
@article{paperbot719,
title = {POPLMark reloaded: Mechanizing proofs by logical relations},
author = {ANDREAS ABEL and GUILLAUME ALLAIS and ALIYA HAMEER and BRIGITTE PIENTKA and ALBERTO MOMIGLIANO and STEVEN SCHÄFER and KATHRIN STARK},
journal = {Journal of Functional Programming},
volume = {29},
year = {2019},
doi = {10.1017/s0956796819000170}
}