SHF:Small: Extensible Models and Proofs via Family Polymorphism

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

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.