Powerful User Interfaces for Interactive Theorem Proving

软件在航空、医疗设备和其他安全和关键任务中的作用越来越大，这推动了学术界和工业界对软件验证的重大研究。这一努力涉及到使用形式化的数学方法证明，软件做了它的作者想要它做的事情。交互式定理证明器（ITP）是软件验证中的关键工具，使用户能够创建自动证明器无法实现的深度属性的复杂证明。尽管越来越需要使用ITP，但ITP的用户界面有限，在过去20年中几乎没有发展。这使得新手很难开始使用这些工具，并限制了专家的生产力。本研究的目的是设计，开发和评估功能强大的用户界面的ITP。由此产生的用户界面将作为开放源代码免费提供给公众，假设是，通过先进的编辑技术满足ITP用户信息需求的新型ITP用户界面将使新手能够比目前的ITP用户界面更快、更准确地证明定理和理解证明，并提高有经验用户的生产力。先进的编辑技术将包括推理规则和复杂的语法可视化和操纵，以及证明预览。总之，这些技术将使用户能够了解证明是如何发展的，更容易阅读复杂的公式，并快速探索推进证明的方法。该假设将使用Coq进行检验，Coq是一种广泛采用的ITP。对高级编辑技术的评价将包括在完成和理解证明的效率方面与广泛使用的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.