Frex: dependently-typed algebraic simplification
Programming Languages
2025-07-21 v2 Logic in Computer Science
Symbolic Computation
Abstract
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.
Keywords
Cite
@article{arxiv.2306.15375,
title = {Frex: dependently-typed algebraic simplification},
author = {Guillaume Allais and Edwin Brady and Nathan Corbyn and Ohad Kammar and Jeremy Yallop},
journal= {arXiv preprint arXiv:2306.15375},
year = {2025}
}