News & Events
A talk by Donnacha Oisin Kidney
Tuesday 27th November 2018, WGB G02 4-5pm
Title: An efficient and flexible evidence-providing solver for polynomial equalities in Agda
Speaker:Donnacha Oisin Kidney
We present a new implementation of a ring solver in the programming language Agda. The new implementation is significantly more efficient than the version in the standard library, bringing it in line with Coq’s ring tactic.
We demonstrate techniques for constructing proofs based on the theory of lists, show how Agda’s reflection system can be used to provide a safe and simple interface to the solver, and compare the “correct by construction” approach to that of auxiliary proofs.
We also show that, as a by-product of proving equivalences rather than equalities, the prover can be used to provide artefacts other than equational proofs, including pedagogical step-by-step solutions, and isomorphisms.