课题基金 / 基金详情

Improving the Nuprl Proof Development System

Improving the Nuprl Proof Development System
改进Nuprl证明开发系统
批准号:
9002822
负责人:
Robert Constable
金额:
$0.0万
依托单位:
依托单位国家:
美国
项目类别:
Standard Grant
财政年份:
1990
资助国家:
美国
项目状态:
已结题
起止时间:
1990-06-01 至 1991-05-31

项目摘要

项目成果

Robert Constable的其他基金

相似基金

相关文献

中文摘要
翻译
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.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
EAGER: Constructive Univalent Foundations
  • 批准号:
    1650069
  • 项目类别:
    Standard Grant
  • 资助金额:
    $29.5万
  • 财政年份:
    2016
  • 负责人:
    Robert Constable
  • 依托单位:
CSR-EHS: Developing a Theory of Events to Improve Distributed Systems
  • 批准号:
    0614790
  • 项目类别:
    Continuing grant
  • 资助金额:
    $0.0万
  • 财政年份:
    2006
  • 负责人:
    Robert Constable
  • 依托单位:
Enabling Large-Scale Coherency Among Mathematical Texts in the NSDL
  • 批准号:
    0333526
  • 项目类别:
    Standard Grant
  • 资助金额:
    $46.0万
  • 财政年份:
    2003
  • 负责人:
    Robert Constable
  • 依托单位:
Innovative Programming Technology for Embedded Systems
  • 批准号:
    0208536
  • 项目类别:
    Continuing grant
  • 资助金额:
    $30.0万
  • 财政年份:
    2002
  • 负责人:
    Robert Constable
  • 依托单位:
海外基金