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

点击翻译按钮获取中文摘要

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.