Improving the Nuprl Proof Development System

NUPRL是一个支持形式数学交互发展的系统。它被设计成特别适合于计算意义重大的数学和正式验证的软件的构造。由国家科学基金会资助的NUPRL的实施工作于1984年完成。从那时起，该系统在康奈尔大学和其他地方被广泛使用，作为进一步研究的基础。这项研究在自动推理和计算逻辑领域取得了重大进展。该系统已成功地应用于从计算机硬件验证到程序设计语言理论中的一个公开问题的广泛问题。它已经成为许多文章和博士论文的主题。本项目的目标是重写系统的某些部分，以便纳入某些扩展(反映机制)和改进(新的定义工具)。这些都是基于几年来对该系统的研究和经验。他们将使该系统更容易被该地区的研究人员以及数学家和教育工作者等其他人访问。随着反射机制的实施，Nuprl将适用于目前难以处理的领域。

Nuprl is a system supporting the interactive development of formal mathematics. It was designed to be especially suited to computationally significant mathematics and to the construction of formally verified software. The implementation of Nuprl, funded by the NSF, was completed in 1984. Since then the system has been used extensively at Cornell and elsewhere as a basis for further research. This research has resulted in significant advances in the areas of automated reasoning and computational logic. The system has been successfully applied to a wide range of problems, from verification of computer hardware to an open problem in the theory of programming languages. It has been the subject of many articles and PhD theses. The goal of the present project is to rewrite parts of the system in order to incorporate certain extensions (a reflection mechanism) and improvements (new definition facility). These are based on several years of study and experience with the system. They will make the system more accessible, both to researchers in the area and to others such as mathematicians and educators. With the implementation of the reflection mechanism, Nuprl will be applicable to domains that are currently difficult to treat.