Powerful User Interfaces for Interactive Theorem Proving

软件在航空、医疗设备和其他安全和任务关键型任务中的作用越来越大，这推动了学术界和工业界在软件验证方面的重大研究工作。这项工作包括使用正式的数学方法来证明软件做了它的作者想要做的事情。交互式定理证明器(ITP)是软件验证中的关键工具，使用户能够创建自动证明器无法触及的深层性质的复杂证明。尽管对ITP的使用需求日益增加，但ITP的用户界面有限，在过去20年里几乎没有发展过。这使得新手很难开始使用这些工具，并限制了专家的工作效率。本研究的目的是设计、开发和评估ITP的强大用户界面。由此产生的用户界面将以开源代码的形式向公众免费提供。假设通过先进的编辑技术满足ITP用户的信息需求的新型ITP用户界面将使新手能够比目前的ITP用户界面更快、更准确地证明定理和理解证明，并提高有经验的用户的生产力。高级编辑技术将包括推理规则和复杂的语法可视化和操作，以及证据预览。这些技术结合在一起，将使用户能够了解校样是如何演变的，更容易阅读复杂的公式，并快速探索推进校样的方法。这一假设将使用被广泛采用的ITP-CoQ进行检验。对先进编辑技术的评价将包括与广泛使用的ITP用户界面在完成和理解校样方面的效率的比较。成功地将现代人机交互技术应用于交互式定理证明者，将使ITP的可用性和适用性向前迈进一大步。这反过来将有助于促进在学术研究中以及在工业应用中更多地使用正式方法和验证。同样，它将为教授软件验证课程提供一个有用的工具，帮助学生专注于证明定理，而不是将注意力集中在如何与软件交互上。项目成果将通过提交给人机交互场馆和交互定理证明者的方式传播。

Software's increasing role in aviation, medical devices, and other safety- and mission-critical tasks is driving a major research effort in software verification, in both academia and industry. This effort involves proving, using formal mathematical methods, that software does what its authors intend it to do. Interactive theorem provers (ITPs) are a key tool in software verification, enabling users to create complex proofs of deep properties beyond the reach of automated provers. In spite of the increasing need for their use, ITPs have limited user interfaces that have hardly evolved in the past 20 years. This makes it difficult for novices to begin using these tools, and limits the productivity of experts. The objective of this research is to design, develop, and evaluate powerful user interfaces for ITPs. The resulting user interfaces will be made freely available to the public as open-source code.The hypothesis is that a novel ITP user interface that addresses ITP users' information needs through advanced editing techniques will enable novices to prove theorems and understand proofs more quickly and accurately than current ITP user interfaces, and increase productivity for experienced users. Advanced editing techniques will include inference rule and complex syntax visualization and manipulation, as well as proof previews. Together, these techniques will enable users to understand how proofs evolve, more easily read complex formulas, and quickly explore ways of advancing a proof. The hypothesis will be tested using Coq, a widely adopted ITP. The evaluation of the advanced editing techniques will include a comparison with a widely used ITP user interface in terms of efficiency for completing and understanding proofs. Successfully applying modern human-computer interaction techniques to interactive theorem provers will result in a major step forward in the usability and applicability of ITPs. This in turn will help facilitate the increased use of formal methods and verification in academic research, but also with industrial applications. Likewise, it will provide a useful tool for teaching software verification courses by helping students concentrate on proving theorems instead of focusing their attention on how to interact with software. Project results will be disseminated by submission to venues in human-computer interaction and interactive theorem provers.