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

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

• 批准号: 2203217
• 负责人: Patricia Johann
• 金额: $ 61.31万
• 依托单位: Appalachian State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2203217&HistoricalAwards=false
• 关键词: SHF; Small; RUI; Deep; Induction

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产生的结构诱导规则无法证明。深度诱导是对结构诱导的最近发展的概括，它确实对数据结构中存在的所有数据确实具有诱导。该项目的新颖性是，它从代数数据类型（ADT）和（真正的）嵌套类型延伸到COQ通常通过COQ处理的嵌套类型的深度诱导，以将其更具表现力的概括（gadts）和感应性家族（IF）（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）一种新型的内型函数初始代数式语义，用于GADTS，证明其深度归纳规则； iii）gadts和IFS之间的翻译对IFS产生相似的语义，从而产生类似的诱导规则； iv）实施了为GADT和IFS生成深层归纳规则的工具，以及直接从其语法中证明其正确的证人。总体而言，该项目应用最先进的理论来改善最新的验证实践。从理论上讲，本机的初始代数语义是数据类型理论的基石之一，也是为它们得出结构性诱导规则的关键。该项目的深层吸引力框架的一个特别引人注目的特征是，GADT和用作其基础的IF的新颖的“最大功能解释”基于与ADT和嵌套类型的标准初始代数语义相同，并且确实专门针对标准的初始代数语义。因此，它为ADT，（真正的）嵌套类型，GADT和IFS提供了统一的语义，以及一种用于得出其深层归纳规则的统一方法。实际上，这可以通过保守地扩展当前用于ADT的标准归纳技术而不是通过开发根本新的新方法来将GADT和IFS的深层归纳纳入现代证明助手。即使仅将ADT的深层归纳纳入现有证明助手也将大大扩展和改进。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的知识分子优点和更广泛的影响审查标准通过评估来获得支持的。