Design and Implementation of Family Polymorphism for Interactive Theorem Proving
| dc.contributor.author | Jin, Ende | |
| dc.date.accessioned | 2023-06-13T18:41:49Z | |
| dc.date.available | 2023-06-13T18:41:49Z | |
| dc.date.issued | 2023-06-13 | |
| dc.date.submitted | 2023-06-07 | |
| dc.description.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. | en |
| dc.identifier.uri | http://hdl.handle.net/10012/19531 | |
| dc.language.iso | en | en |
| dc.pending | false | |
| dc.publisher | University of Waterloo | en |
| dc.subject | proof engineering | en |
| dc.subject | interactive theorem proving | en |
| dc.subject | expression problem | en |
| dc.subject | inductive types | en |
| dc.subject | extensible frameworks | en |
| dc.subject | modules | en |
| dc.subject | mixins | en |
| dc.subject | reuse | en |
| dc.subject | dependent type theory | en |
| dc.subject | Coq | en |
| dc.title | Design and Implementation of Family Polymorphism for Interactive Theorem Proving | en |
| dc.type | Master Thesis | en |
| uws-etd.degree | Master of Mathematics | en |
| uws-etd.degree.department | David R. Cheriton School of Computer Science | en |
| uws-etd.degree.discipline | Computer Science | en |
| uws-etd.degree.grantor | University of Waterloo | en |
| uws-etd.embargo.terms | 0 | en |
| uws.contributor.advisor | Zhang, Yizhou | |
| uws.contributor.advisor | Lhoták, Ondřej | |
| uws.contributor.affiliation1 | Faculty of Mathematics | en |
| uws.peerReviewStatus | Unreviewed | en |
| uws.published.city | Waterloo | en |
| uws.published.country | Canada | en |
| uws.published.province | Ontario | en |
| uws.scholarLevel | Graduate | en |
| uws.typeOfResource | Text | en |