Design and Implementation of Family Polymorphism for Interactive Theorem Proving
Loading...
Date
2023-06-13
Authors
Jin, Ende
Journal Title
Journal ISSN
Volume Title
Publisher
University of Waterloo
Abstract
With the growing practice of mechanizing language metatheories, it has become ever more pressing that interactive theorem provers make it easy to write reusable, extensible code and proofs.
This thesis presents a novel language design geared towards extensible metatheory mechanization in a proof assistant. The new design achieves reuse and extensibility via a form of family polymorphism, an object-oriented idea, that allows code and proofs to be polymorphic to their enclosing families. Our development addresses technical challenges that arise from the underlying language of a proof assistant being simultaneously functional, dependently typed, a logic, and an interactive tool. Our
results include (1) a prototypical implementation of the language design as a Coq plugin, (2) a dependent type theory capturing the essence of the language mechanism and its consistency and canonicity results, and (3) case studies showing how the new expressiveness naturally addresses real programming challenges in metatheory mechanization.
Description
Keywords
proof engineering, interactive theorem proving, expression problem, inductive types, extensible frameworks, modules, mixins, reuse, dependent type theory, Coq