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.