课题基金 / 基金详情

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的实施,由 NSF于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
  • 依托单位:
海外基金