SHF:Small: Extensible Models and Proofs via Family Polymorphism

Proof Assistant支持模型的交互式开发及其机器检查的证明。这些发展保证了模型具有某些属性，如系统的安全性、正确性和可靠性。它们也被用作教学工具，例如在编程语言语义的课程中。不幸的是，像Coq这样的证明助手缺乏一种可扩展的模型和证明设计机制。今天，当一个模型及其相应的证明需要扩展时，开发人员通常会复制粘贴开发并手动传播更改。这就导致了相互之间没有联系和相互重复的发展扩散，模糊了概念。该项目为证明助手带来了模型和证明的内置可扩展性。特别是，它优先考虑代码重用，代码模块化和扩展的可靠性。该项目还旨在为用户提供直观的可扩展性，并将对用户体验的干扰降至最低。该项目的新颖之处在于内置的可扩展性--因为相关的解决方案主要是附加组件或插件，以及使用家族多态性来支持证明的可扩展性。该项目的影响是对不断发展的系统进行快速、增量的验证，验证设置中的代码模块化和重用，以及降低初学者进入验证的门槛。该项目将家族多态性带到了验证助手的世界。家族多态性是编程语言理论中的一种机制，通过它可以完整地继承特征家族。族提供了组织上的好处，比如代码模块化，以及可扩展性的好处，比如在存在继承的情况下代码的类型安全。家族多态性将支持模型和证明的可扩展设计，促进代码重用和证明重用。此外，它将有可能指定和证明家庭多态保证任何健全的家庭来自一个基本家庭。如果派生族满足从基族继承的所有证明义务，则派生族是可靠的。族多态性支持"垂直"扩展（其中功能在单个层次结构中扩展）和"水平"扩展（其中功能独立组合）。后者是在Scala等系统中通过traits和mixin组合实现的。由于嵌套的家族多态性支持对mixin组合进行编码，因此可以对垂直和水平扩展使用相同的机制。这个项目使用家族多态性作为证明设置的扩展策略集的统一机制。面临的挑战包括集成家庭多态性和扩展性策略与依赖类型理论的证明助手，找到策略，以重用证明以及模型，并使实际使用的无缝集成。鉴于这些挑战，该项目研究了与证明助手中的模块化重用相关的三个主要领域：（1）元理论，（2）策略，（3）实现。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Proof assistants enable interactive development of models and their machine-checked proofs. These developments provide guarantees that a model has certain properties, such as security, correctness, and soundness of systems. They are also used as a teaching vehicle, for example in classes on the semantics of programming languages. Unfortunately, proof assistants such as Coq lack a mechanism for extensible design of models and proofs. Today, when a model and its corresponding proofs need to be extended, developers typically copy-paste the development and manually propagate the changes. This leads to a proliferation of developments that are not linked together and that duplicate one another, obscuring concepts. This project brings built-in extensibility of models and proofs to proof assistants. In particular, it prioritizes code reuse, code modularity, and soundness of extensions. The project also aims to make extensibility intuitive for the user and a minimal disruption to the user experience. The project’s novelties are the built-in nature of extensibility — since related solutions are largely add-ons or plug-ins, as well as the use of family polymorphism to support extensibility of proofs. The project’s impacts are the rapid, incremental verification of evolving systems, code modularity and reuse in the proof setting, and lowered barriers to entry for beginners in verification.This project brings family polymorphism to the world of proof assistants. Family polymorphism is a mechanism in the theory of programming languages by which families of features can be inherited integrally. Families provide organizational benefits, such as code modularity, as well as extensibility benefits, such as type safety of code in the presence of inheritance. Family polymorphism will support extensible designs of models and proofs, facilitating code reuse and proof reuse. Furthermore, it will be possible to specify and prove family-polymorphic guarantees for any sound family derived from a base family. A derived family is sound if it satisfies all the proof obligations inherited from a base family. Family polymorphism supports both a “vertical” extension, where features are extended in a single hierarchy, as well as “horizontal” extension, where features are combined independently. The latter is achieved with traits and mixin composition in systems such as Scala. Since nested family polymorphism enables the encoding of mixin composition, the same mechanism for both vertical and horizontal extensions can be used. This project uses family polymorphism as a unifying mechanism for its set of extensibility strategies for the proof setting. The challenges include integrating family polymorphism and extensibility strategies with the dependent type theory of proof assistants, finding strategies to reuse proofs as well as models, and making the integration seamless for practical use. Informed by these challenges, the project researches three main areas related to modular reuse in proof assistants: (1) meta-theories, (2) strategies, and (3) implementations.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.