不要打电话给我们，我们会打给你：迈向面向编程语言理论的混合主动交互式证明助手
Don't Call Us, We'll Call You: Towards Mixed-Initiative Interactive Proof Assistants for Programming Language Theory
AI总结：
针对语义工程工具与证明助手脱节问题，提出一种由自动证明搜索开始并在需用户反馈时中断的混合主动交互模式，构建小型证明助手验证了其能简化证明构建。
摘要：
编程语言研究人员在工作中使用两类系统。语义工程工具允许他们交互式地探索其定义，而证明助手可用于检查其特性的证明。这两类系统之间的脱节导致了已发表论文中的错误，并限制了在编写证明时可用的交互模式。在构建证明时，通常的做法是先陈述属性，然后手动开发证明，直到自动策略能够填补剩余的空白。我们认为，利用编程语言典型结构的集成且更具交互性的工具可以做得更好。一个了解编程语言证明典型结构的证明助手可能需要更少的人工输入，帮助用户理解他们的证明，同时还能利用来自可执行语义探索的见解来进行证明构建。在本文提出的早期工作中，我们专注于与证明助手交互的问题，并将语义工程部分留待未来研究。我们提出了一种工作方式，不是从手动证明构建开始然后自动完成最后几步，而是由工具从自动证明搜索开始，然后在需要用户反馈时中断。我们构建了一个遵循这种交互模式的小型证明助手，并使用 Peano 算术中“+”运算交换律的简单证明来阐述这一想法。我们的早期经验表明，这种工作方式可以使证明构建更容易。
英文摘要：
There are two kinds of systems that programming language researchers use for their work. Semantics engineering tools let them interactively explore their definitions, while proof assistants can be used to check the proofs of their properties. The disconnect between the two kinds of systems leads to errors in accepted publications and also limits the modes of interaction available when writing proofs. When constructing a proof, one typically states the property and then develops the proof manually until an automatic strategy can fill the remaining gaps. We believe that an integrated and more interactive tool that leverages the typical structure of programming language could do better. A proof assistant aware of the typical structure of programming language proofs could require less human input, assist the user in understanding their proofs, but also use insights from the exploration of executable semantics in proof construction. In the early work presented in this paper, we focus on the problem of interacting with a proof assistant and leave the semantics engineering part to the future. Rather than starting with manual proof construction and then completing the last steps automatically, we propose a way of working where the tool starts with an automatic proof search and then breaks when it requires feedback from the user. We build a small proof assistant that follows this mode of interaction and illustrates the idea using a simple proof of the commutativity of the "+" operation for Peano arithmetic. Our early experience suggests that this way of working can make proof construction easier.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
