Please use this identifier to cite or link to this item:
http://hdl.handle.net/11375/26272
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.advisor | Carette, Jacques | - |
dc.contributor.advisor | Farmer, William | - |
dc.contributor.author | Sharoda, Yasmine | - |
dc.date.accessioned | 2021-03-31T18:28:52Z | - |
dc.date.available | 2021-03-31T18:28:52Z | - |
dc.date.issued | 2021 | - |
dc.identifier.uri | http://hdl.handle.net/11375/26272 | - |
dc.description.abstract | Building a large library of mathematical knowledge is a complex and labour-intensive task. By examining current libraries of mathematics, we see that the human effort put in building them is not entirely directed towards tasks that need human creativity. Instead, a non-trivial amount of work is spent on providing definitions that could have been mechanically derived. In this work, we propose a generative approach to library building, so definitions that can be automatically derived are computed by meta-programs. We focus our attention on libraries of algebraic structures, like monoids, groups, and rings. These structures are highly inter-related and their commonalities have been well-studied in universal algebra. We use theory presentation combinators to build a library of algebraic structures. Definitions from universal algebra and programming languages meta-theory are used to derive library definitions of constructions, like homomorphisms and term languages, from algebraic theory presentations. The result is an interpreter that, given 227 theory expressions, builds a library of over 5000 definitions. This library is, then, exported to Agda and Lean. | en_US |
dc.language.iso | en | en_US |
dc.subject | formal methods | en_US |
dc.subject | algebra library | en_US |
dc.subject | theorem provers | en_US |
dc.subject | theory development | en_US |
dc.title | Leveraging Information Contained in Theory Presentations | en_US |
dc.type | Thesis | en_US |
dc.contributor.department | Computer Science | en_US |
dc.description.degreetype | Dissertation | en_US |
dc.description.degree | Doctor of Philosophy (PhD) | en_US |
Appears in Collections: | Open Access Dissertations and Theses |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Sharoda_Yasmine_2021March_PhD.pdf | 1.82 MB | Adobe PDF | View/Open |
Items in MacSphere are protected by copyright, with all rights reserved, unless otherwise indicated.