On Friday October 17, this site was moved to a new server, https://mw.hh.se. The original address will continue to work. Whithin a week or two this site will return to the original address. /Peo HH IT-dep

WG211/M25Yallop

From WG 2.11
Revision as of 17:07, 7 November 2025 by Jacques (talk | contribs) (Created page with "(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's dependently typed interface guarantees that both built-in and user-defined simplification modules are terminating, sound, and complete with respect to a well...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

(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's dependently typed interface guarantees that both built-in and user-defined simplification modules are terminating, sound, and complete with respect to a well-specified class of equations.

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.

Retrieved from "http://mw.hh.se/wg211/index.php?title=WG211/M25Yallop&oldid=2813"