EAGER: Constructive Univalent Foundations

EAGER：建设性的单价基础

• 批准号: 1650069
• 负责人: Robert Constable
• 金额: $ 29.5万
• 依托单位: Cornell University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-09-01 至 2019-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1650069&HistoricalAwards=false
• 关键词: EAGER; Constructive; Univalent; Foundations

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.

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