EAGER: Constructive Univalent Foundations

证明助手可以用形式逻辑系统来表示任何精确的计算任务。它们准确地规定了操作和使用规范来指导实现所需的硬件和软件。在过去的二十年里，使用这些工具的计算机科学家已经取得了已知的最高水平的正确性。证明助手利用高等数学；他们已经被用来检查几个深刻的数学结果的有效性，并发现新的结果。在这个过程中，顶尖的数学家为形式逻辑贡献了强大的新概念。菲尔兹奖牌获得者弗拉基米尔·沃沃茨基提出了一种新的数学原理，称为单价。这一原理是否具有计算解释一直是一个悬而未决的问题。这个问题最近得到了PI和他的合作者的肯定回答。这个项目的智力价值在于使用证明助手对这些解释的正确性进行正式验证。该项目的更广泛的意义和重要性是增强它们对计算系统在科学、工程和工业中的许多关键应用的影响，并探索它们在高中生欧几里德几何教学中的应用。这个关于建设性单叶基础的研究项目显著提高了证明助手可以支持的抽象水平，并增加了他们帮助解决的问题的范围。PI和他的团队的初步结果提供了强有力的证据，表明单价基础和使用它的计算类型理论将显著提高证明助手的能力，从而提高从桌面到云的现代计算系统所依赖的硬件和软件的可靠性和能力。该项目正式验证了过去三十年来由PI及其合作者开发的证明助手Nuprl中单价计算解释的正确性。

Proof assistants can express any precise computing task in formal systems of logic. They specify exactly how hardware and software are required to operate and use the specifications to guide implementations. Computer scientists using these tools have achieved over the past two decades the highest levels of correctness known. Proof assistants draw on advanced mathematics; they have been used to check the validity of several deep mathematical results and discover new ones. In this process, leading mathematicians contributed powerful new concepts into the formal logics. Fields Medalist Vladimir Voevodsky proposed a new mathematical principle, called Univalence. It has been an open question whether this principle has computational interpretations. That question was affirmatively answered recently by the PI and his collaborators. The intellectual merits of this project consist in formal verification of the correctness of these interpretations using a proof assistant. The project's broader significance and importance are to enhance their impact on many critical applications of computing systems in science, engineering, and industry and to explore their use in teaching Euclidean geometry to high school students.This research project on Constructive Univalent Foundations significantly raises the levels of abstraction that proof assistants can support, and increases the range of problems they help solve. Preliminary results by the PI and his team provide strong evidence that Univalent Foundations and the computational type theory using it will significantly improve the capabilities of proof assistants and thus the reliability and capabilities of hardware and software on which modern computing systems depend, from the desktop to the cloud. The project formally verifies the correctness of the computational interpretations of Univalence in the proof assistant Nuprl that has been developed by the PI and his collaborators over the last three decades.