SHF:Small: Extensible Models and Proofs via Family Polymorphism

校样助手可以交互开发模型及其机器检查的校样。这些开发提供了模型具有某些属性的保证，例如系统的安全性、正确性和健全性。它们也被用作教学工具，例如在编程语言语义学的课堂上。不幸的是，诸如Coq这样的证明助手缺乏用于模型和证明的可扩展设计的机制。如今，当一个模型及其相应的证明需要扩展时，开发人员通常会复制-粘贴开发并手动传播更改。这导致了没有联系、相互重复的发展的激增，使概念变得模糊。这个项目为验证助手带来了模型和证明的内置可扩展性。特别是，它优先考虑代码重用、代码模块化和扩展的健壮性。该项目还旨在使可扩展性对用户来说更直观，并将对用户体验的干扰降至最低。该项目的新奇之处在于可扩展性的内置性质--因为相关的解决方案主要是加载项或插件，以及使用家族多态来支持校样的可扩展性。该项目的影响是快速、增量地验证不断发展的系统，在证明设置中代码模块化和重用，并降低了初学者在验证中的进入门槛。该项目为证明助理世界带来了家庭多态。家族多态是编程语言理论中的一种机制，通过它可以完整地继承一系列特征。族提供了组织方面的好处，例如代码模块化，以及可扩展性方面的好处，例如在继承的情况下代码的类型安全。家族多态将支持模型和证明的可扩展设计，促进代码重用和证明重用。此外，还可以为从基本家族派生的任何健全的家族指定和证明家族多态保证。如果一个派生族满足从基族继承的所有证明义务，则它是健全的。家族多态支持“垂直”扩展和“水平”扩展，前者在单个层次结构中扩展功能，后者功能独立组合。后者是通过Scala等系统中的特征和混合成分实现的。由于嵌套家族多态能够对混合蛋白成分进行编码，因此可以对垂直和水平扩展使用相同的机制。该项目使用家族多态作为其用于证明设置的可扩展性策略集的统一机制。挑战包括将家族多态和可扩展性策略与证明助手的依赖类型理论相结合，找到重复使用证明和模型的策略，以及使集成无缝地用于实际用途。受这些挑战的启发，该项目研究了与证明助手中的模块化重用相关的三个主要领域：(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.