http://mw.hh.se/wg211/index.php?action=history&feed=atom&title=WG211%2FM25Yallop 2026-04-05T21:09:14Z Revision history for this page on the wiki MediaWiki 1.43.5 http://mw.hh.se/wg211/index.php?title=WG211/M25Yallop&diff=2813&oldid=prev 2025-11-07T16:07:58Z

<p>Created page with &quot;(joint work with Guillaume Allais, Edwin Brady, Nathan Corbyn and Ohad Kammar) We present a new design for an algebraic simplification library structured around concepts from universal algebra: theories, models, homomorphisms, and universal properties of free algebras and free extensions of algebras. The library&#039;s dependently typed interface guarantees that both built-in and user-defined simplification modules are terminating, sound, and complete with respect to a well...&quot;</p> <p><b>New page</b></p><div>(joint work with Guillaume Allais, Edwin Brady, Nathan Corbyn and Ohad Kammar)<br /> <br /> We present a new design for an algebraic simplification library structured around concepts from universal algebra: theories,<br /> models, homomorphisms, and universal properties of free algebras and free extensions of algebras.<br /> <br /> The library&#039;s dependently typed interface guarantees that both built-in and user-defined simplification modules are terminating,<br /> sound, and complete with respect to a well-specified class of equations.<br /> <br /> We have implemented the design in the Idris 2 and Agda dependently typed programming languages and shown that it supports modular extension to new theories, proof extraction and certification, goal extraction via reflection, and interactive development.</div>

Jacques