一个支持绑定器的开放式挑战问题库
An Open Challenge Problem Repository for Systems Supporting Binders
摘要：
各种逻辑框架支持使用高阶抽象语法来表示正式系统;然而，每个系统都有自己的基准集。更糟糕的是，一般的证明助手提供了处理绑定器的特殊库，对这些库的评估非常有限，并且给出的示例通常没有对绑定器存在时出现的关键方面进行练习和压力测试。在本文中，我们设计了一个开放的知识库ORBI（开放的挑战问题库系统支持推理与绑定）。我们相信，使用绑定器对语言进行推理的领域已经成熟，一组通用的基准测试为评估和定性比较支持绑定器的不同系统和库提供了重要的基础，这将有助于推动该领域的发展。
英文摘要：
A variety of logical frameworks support the use of higher-order abstract syntax in representing formal systems; however, each system has its own set of benchmarks. Even worse, general proof assistants that provide special libraries for dealing with binders offer a very limited evaluation of such libraries, and the examples given often do not exercise and stress-test key aspects that arise in the presence of binders. In this paper we design an open repository ORBI (Open challenge problem Repository for systems supporting reasoning with BInders). We believe the field of reasoning about languages with binders has matured, and a common set of benchmarks provides an important basis for evaluation and qualitative comparison of different systems and libraries that support binders, and it will help to advance the field.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
