Frex : dependently typed algebraic simplification

Tools

Allais, Guillaume and Brady, Edwin and Corbyn, Nathan and Kammar, Ohad and Yallop, Jeremy (2025) Frex : dependently typed algebraic simplification. Proceedings of the ACM on Programming Languages (PACMPL), 9 (ICFP). pp. 30-65. 237. ISSN 2475-1421 (https://doi.org/10.1145/3747506)

[thumbnail of Allais-etal-PACMPL-2025-Frex-dependently-typed-algebraic-simplification]
Preview
 Text. Filename: Allais-etal-PACMPL-2025-Frex-dependently-typed-algebraic-simplification.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (938kB)| Preview

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.

ORCID iDs

Allais, Guillaume ORCID logoORCID: https://orcid.org/0000-0002-4091-657X, Brady, Edwin, Corbyn, Nathan, Kammar, Ohad and Yallop, Jeremy;
CORE (COnnecting REpositories)