BSc thesis.
We present a new library which automates the construction of equivalence proofs between polynomials over commutative rings and semirings in the programming language Agda. It is significantly faster than Agda’s existing solver. We use reflection to provide a sim- ple interface to the solver, and demonstrate how to use the constructed proofs to provide step-by-step solutions.
Bibtex:
@phdthesis{kidneyAutomaticallyEfficientlyIllustrating2019,
type = {Bachelor Thesis},
title = {Automatically and {{Efficiently Illustrating Polynomial Equalities}} in {{Agda}}},
author = {Kidney, Donnacha Ois{\'i}n},
year = {2019},
month = apr,
address = {{Cork, Ireland}},
url = {https://doisinkidney.com/pdfs/bsc-thesis.pdf},
abstract = {We present a new library which automates the construction of equivalence proofs between polynomials over commutative rings and semirings in the programming language Agda. It is signi cantly faster than Agda's existing solver. We use re ection to provide a sim- ple interface to the solver, and demonstrate how to use the constructed proofs to provide step-by-step solutions.},
langid = {english},
school = {University College Cork}
}