SHF:Small: Extensible Models and Proofs via Family Polymorphism

Harvard University, Cambridge MA

Investigators

Abstract

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.