Powerful User Interfaces for Interactive Theorem Proving

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

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.