News & Events

A talk by Donnacha Oisin Kidney

23 Nov 2018

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.

School of Mathematical Sciences

Eolaíochtaí Matamaiticiúla

Room 1-57, First Floor floor, T12 XF62