SHF:Small:RUI: Deep Induction Rules for Advanced Data Types

SHF:Small:RUI:高级数据类型的深度归纳规则

基本信息

  • 批准号:
    2203217
  • 负责人:
  • 金额:
    $ 61.31万
  • 依托单位:
  • 依托单位国家:
    美国
  • 项目类别:
    Standard Grant
  • 财政年份:
    2022
  • 资助国家:
    美国
  • 起止时间:
    2022-10-01 至 2025-09-30
  • 项目状态:
    未结题

项目摘要

A particularly successful approach to software verification is deductive verification. Deductive verification generates mathematical proof obligations from software specifications, and, when these proof obligations are met, software implementations are guaranteed to conform to the specifications from which they were generated. Generated obligations can be discharged by means of hand-written mathematical proofs, but modern software is sufficiently complex that this is often tedious and error-prone, if not outright infeasible. Increasingly, therefore, proofs are developed in proof assistants like Agda, Coq, Idris, and Lean. Induction is one of the most important proof techniques available in such proof assistants. Indeed, almost all non-trivial proofs involving data types are either proved by induction outright or rely on lemmas that are. For this reason, every time a new data type is declared in, say, Coq, an induction rule is automatically generated for it. But because they traverse only the top layer, rather than all of the layers of a data structure, there are some properties of data types that should be amenable to induction but that the structural induction rules generated by Coq cannot prove. Deep induction is a recently developed generalization of structural induction that does indeed induct over all of the data present in data structures. This project's novelty is that it extends deep induction from the algebraic data types (ADTs) and (truly) nested types typically handled by Coq to their more expressive generalizations known as generalized ADTs (GADTs) and inductive families (IFs). The project's impact is thus to make it possible to detect errors and verify program properties that cannot be expressed just using ADTs and nested types, but that can be expressed using GADTs and IFs.The project involves developing a principled, conceptually simple, uniform, and comprehensive framework for deep induction for GADTs and IFs, including: i) a grammar that generates a very general class of GADTs, including all those from the literature; ii) a novel endofunctor initial-algebra-like semantics for GADTs that justifies their deep induction rules; iii) translations between GADTs and IFs that yield similar semantics, and thus deep induction rules, for IFs; and iv) implemented tools that generate deep induction rules for GADTs and IFs, together with witnesses that prove them correct, directly from their syntax. Overall, the project applies state-of-the-art theory to improve state-of-the-art verification practice. Theoretically, endofunctor initial algebra semantics is one of the cornerstones of the theory of data types, and is key to deriving even structural induction rules for them. A particularly compelling feature of the project's framework for deep induction is that the novel "maximally functorial interpretations" of GADTs and IFs that serve as its foundation are based on the same well-established principles as, and indeed specialize to, the standard initial algebra semantics for ADTs and nested types. It thus delivers a uniform semantics for ADTs, (truly) nested types, GADTs, and IFs, as well as a uniform methodology for deriving their deep induction rules. Practically speaking, this makes it possible to incorporate deep induction for GADTs and IFs into modern proof assistants by conservatively extending the standard induction techniques currently in use for ADTs, rather than by developing fundamentally new approaches. Even incorporating deep induction just for ADTs into existing proof assistants will significantly extend and improve them.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.
一个特别成功的软件验证方法是演绎验证。演绎验证从软件规范中生成数学证明义务,并且当这些证明义务得到满足时,保证软件实现符合生成它们的规范。生成的义务可以通过手写的数学证明来解除,但现代软件足够复杂,这通常是乏味和容易出错的,如果不是完全不可行的话。因此,越来越多的证明是在像Agda、Coq、Idris和Lean这样的证明助手中开发的。归纳法是此类证明辅助工具中最重要的证明技术之一。事实上,几乎所有涉及数据类型的非平凡证明都是直接通过归纳证明的,或者依赖于这样的引理。因此,每当一个新的数据类型在Coq中被声明时,一个归纳规则就会自动生成,但是因为它们只遍历数据结构的顶层,而不是所有的层,所以数据类型的一些属性应该服从归纳,但是Coq生成的结构归纳规则无法证明。深度归纳是最近发展起来的结构归纳的一种概括,它确实可以归纳数据结构中存在的所有数据。这个项目的新奇在于,它将深度归纳从Coq通常处理的代数数据类型(ADT)和(真正)嵌套类型扩展到更有表现力的泛化,称为广义ADT(GADT)和归纳族(IF)。因此,该项目的影响是使检测错误和验证程序属性成为可能,这些属性不能仅使用ADT和嵌套类型表示,但可以使用GADT和IF表示。该项目涉及为GADT和IF的深度归纳开发一个原则性的、概念简单的、统一的和全面的框架,包括:i)一个生成一个非常一般的GADT类的文法,包括所有来自文献的文法; ii)一个新的GADT类的内函子初始代数语义,证明了它们的深归纳规则; iii)GADT和IF之间的翻译,其产生类似的语义,从而产生IF的深度归纳规则;以及iv)实现的工具,其直接从GADT和IF的语法生成用于GADT和IF的深度归纳规则,以及证明它们正确的证据。总的来说,该项目应用最先进的理论来改进最先进的验证实践。从理论上讲,内函子初始代数语义是数据类型理论的基石之一,并且是推导它们的结构归纳规则的关键。该项目的深度归纳框架的一个特别引人注目的特征是,作为其基础的GADT和IF的新颖的“最大函子解释”基于与ADT和嵌套类型的标准初始代数语义相同的成熟原则,并且专门针对这些原则。因此,它为ADT、(真正的)嵌套类型、GADT和IF提供了统一的语义,以及用于导出其深度归纳规则的统一方法。实际上,这使得有可能通过保守地扩展目前用于ADT的标准归纳技术,而不是通过开发全新的方法,将GADT和IF的深度归纳纳入现代证明助手。即使将ADT的深度归纳纳入现有的证明助手中,也将大大扩展和改进它们。该奖项反映了NSF的法定使命,并通过使用基金会的知识价值和更广泛的影响审查标准进行评估,被认为值得支持。

项目成果

期刊论文数量(0)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)

数据更新时间:{{ journalArticles.updateTime }}

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

数据更新时间:{{ journalArticles.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ monograph.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ sciAawards.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ conferencePapers.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ patent.updateTime }}

Patricia Johann其他文献

Monadic fold, Monadic build, Monadic Short Cut Fusion
Monadic 折叠、Monadic 构建、Monadic 快捷融合
  • DOI:
  • 发表时间:
    2016
  • 期刊:
  • 影响因子:
    0
  • 作者:
    Patricia Johann
  • 通讯作者:
    Patricia Johann
A Productivity Checker for Logic Programming
逻辑编程的生产力检查器
Staged Notational Definitions
分阶段符号定义
  • DOI:
    10.1007/978-3-540-39815-8_6
  • 发表时间:
    2003
  • 期刊:
  • 影响因子:
    0
  • 作者:
    Walid Taha;Patricia Johann
  • 通讯作者:
    Patricia Johann
Lumberjack Summer Camp: A Cross-Institutional Undergraduate Research Experience in Computer Science
伐木工人夏令营:计算机科学的跨机构本科研究经历
  • DOI:
    10.1076/csed.11.4.279.3830
  • 发表时间:
    2001
  • 期刊:
  • 影响因子:
    2.7
  • 作者:
    Patricia Johann;F. Turbak
  • 通讯作者:
    F. Turbak
Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic
结构解析:霍恩子句逻辑中的共归纳证明搜索和证明构造的框架
  • DOI:
  • 发表时间:
    2015
  • 期刊:
  • 影响因子:
    0
  • 作者:
    Ekaterina Komendantskaya;Patricia Johann
  • 通讯作者:
    Patricia Johann

Patricia Johann的其他文献

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

{{ truncateString('Patricia Johann', 18)}}的其他基金

SHF:Small:RUI: Semantic Complexity of Advanced Data Types
SHF:Small:RUI:高级数据类型的语义复杂性
  • 批准号:
    1906388
  • 财政年份:
    2019
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
SHF: Small: RUI: New Foundations for Indexed Programming
SHF:小型:RUI:索引编程的新基础
  • 批准号:
    1713389
  • 财政年份:
    2017
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
SHF: Small: Relational Parametricity for Program Verification
SHF:小:程序验证的关系参数
  • 批准号:
    1420175
  • 财政年份:
    2014
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
Categorical Foundations for Indexed Programming
索引编程的分类基础
  • 批准号:
    EP/G068917/1
  • 财政年份:
    2010
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Research Grant
RUI:Initial Algebra Packages for GADTs: Principled Tools for Structured Programming
RUI:GADT 的初始代数包:结构化编程的原则工具
  • 批准号:
    0700341
  • 财政年份:
    2007
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
RUI: Provable Safety for Performance-Improving Free Theorems-Based Program Transformations
RUI:可证明安全性,可提高性能的基于自由定理的程序转换
  • 批准号:
    0429072
  • 财政年份:
    2004
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Continuing Grant
RUI: Testing and Enhancing a Prototype Program Fusion Engine
RUI:测试和增强原型程序融合引擎
  • 批准号:
    0296006
  • 财政年份:
    2001
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
RUI: Testing and Enhancing a Prototype Program Fusion Engine
RUI:测试和增强原型程序融合引擎
  • 批准号:
    9900510
  • 财政年份:
    1999
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
Mathematical Sciences: Toward a Theory of Well-Founded Orderings for Use in Automated Deduction
数学科学:走向一种用于自动演绎的有根据的排序理论
  • 批准号:
    9696043
  • 财政年份:
    1995
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
Mathematical Sciences: Toward a Theory of Well-Founded Orderings for Use in Automated Deduction
数学科学:走向一种用于自动演绎的有根据的排序理论
  • 批准号:
    9510164
  • 财政年份:
    1995
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant

相似国自然基金

昼夜节律性small RNA在血斑形成时间推断中的法医学应用研究
  • 批准号:
  • 批准年份:
    2024
  • 资助金额:
    0.0 万元
  • 项目类别:
    省市级项目
tRNA-derived small RNA上调YBX1/CCL5通路参与硼替佐米诱导慢性疼痛的机制研究
  • 批准号:
    n/a
  • 批准年份:
    2022
  • 资助金额:
    10.0 万元
  • 项目类别:
    省市级项目
Small RNA调控I-F型CRISPR-Cas适应性免疫性的应答及分子机制
  • 批准号:
    32000033
  • 批准年份:
    2020
  • 资助金额:
    24.0 万元
  • 项目类别:
    青年科学基金项目
Small RNAs调控解淀粉芽胞杆菌FZB42生防功能的机制研究
  • 批准号:
    31972324
  • 批准年份:
    2019
  • 资助金额:
    58.0 万元
  • 项目类别:
    面上项目
变异链球菌small RNAs连接LuxS密度感应与生物膜形成的机制研究
  • 批准号:
    81900988
  • 批准年份:
    2019
  • 资助金额:
    21.0 万元
  • 项目类别:
    青年科学基金项目
肠道细菌关键small RNAs在克罗恩病发生发展中的功能和作用机制
  • 批准号:
    31870821
  • 批准年份:
    2018
  • 资助金额:
    56.0 万元
  • 项目类别:
    面上项目
基于small RNA 测序技术解析鸽分泌鸽乳的分子机制
  • 批准号:
    31802058
  • 批准年份:
    2018
  • 资助金额:
    26.0 万元
  • 项目类别:
    青年科学基金项目
Small RNA介导的DNA甲基化调控的水稻草矮病毒致病机制
  • 批准号:
    31772128
  • 批准年份:
    2017
  • 资助金额:
    60.0 万元
  • 项目类别:
    面上项目
基于small RNA-seq的针灸治疗桥本甲状腺炎的免疫调控机制研究
  • 批准号:
    81704176
  • 批准年份:
    2017
  • 资助金额:
    20.0 万元
  • 项目类别:
    青年科学基金项目
水稻OsSGS3与OsHEN1调控small RNAs合成及其对抗病性的调节
  • 批准号:
    91640114
  • 批准年份:
    2016
  • 资助金额:
    85.0 万元
  • 项目类别:
    重大研究计划

相似海外基金

Collaborative Research: SHF: Small: RUI: CMOS+X: Honey-ReRAM Enabled 3D Neuromorphic Accelerator
合作研究:SHF:小型:RUI:CMOS X:Honey-ReRAM 支持的 3D 神经形态加速器
  • 批准号:
    2247343
  • 财政年份:
    2023
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
Collaborative Research: SHF: Small: RUI: CMOS+X: Honey-ReRAM Enabled 3D Neuromorphic Accelerator
合作研究:SHF:小型:RUI:CMOS X:Honey-ReRAM 支持的 3D 神经形态加速器
  • 批准号:
    2247342
  • 财政年份:
    2023
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
Collaborative Research: SHF: Small: RUI: Keystone: Modular Concurrent Software Verification
协作研究:SHF:小型:RUI:Keystone:模块化并发软件验证
  • 批准号:
    2243636
  • 财政年份:
    2023
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
Collaborative Research: SHF: Small: RUI: Keystone: Modular Concurrent Software Verification
协作研究:SHF:小型:RUI:Keystone:模块化并发软件验证
  • 批准号:
    2243637
  • 财政年份:
    2023
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
Collaborative Research: SHF: Small: RUI: Context-aware Models of Source Code Summarization
协作研究:SHF:小型:RUI:源代码摘要的上下文感知模型
  • 批准号:
    2100050
  • 财政年份:
    2021
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
SHF: Small: Collaborative Research: RUI: Synchronicity: A Framework for Synthesizing Concurrent Software from Sequential and Cooperative Specifications
SHF:小型:协作研究:RUI:同步性:根据顺序和协作规范合成并发软件的框架
  • 批准号:
    1812951
  • 财政年份:
    2018
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
SHF: Small: RUI: New Foundations for Indexed Programming
SHF:小型:RUI:索引编程的新基础
  • 批准号:
    1713389
  • 财政年份:
    2017
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
SHF: Small: RUI: Before, during, and after requirements elicitation interviews: a comprehensive support for improving the quality of requirements
SHF:小:RUI:需求启发访谈之前、期间和之后:为提高需求质量提供全面支持
  • 批准号:
    1718377
  • 财政年份:
    2017
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
SHF: Small: RUI: Characterizing, Detecting, and Fixing Performance Bugs That Have Non-Intrusive Fixes
SHF:小:RUI:表征、检测和修复具有非侵入式修复的性能错误
  • 批准号:
    1644285
  • 财政年份:
    2016
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
SHF: Small: RUI: Characterizing, Detecting, and Fixing Performance Bugs That Have Non-Intrusive Fixes
SHF:小:RUI:表征、检测和修复具有非侵入式修复的性能错误
  • 批准号:
    1528134
  • 财政年份:
    2015
  • 资助金额:
    $ 61.31万
  • 项目类别:
    Standard Grant
{{ showInfoDetail.title }}

作者:{{ showInfoDetail.author }}

知道了