Frex: Dependently typed algebraic simplification

Guillaume Allais; Edwin Brady; Nathan Corbyn; Ohad Kammar; Jeremy Yallop

doi:10.1145/3747506

Frex: Dependently typed algebraic simplification

Guillaume Allais
, Edwin Brady
, Nathan Corbyn
, Ohad Kammar
, Jeremy Yallop

Research output: Contribution to journal › Article › peer-review

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.

Original language	English
Article number	237
Pages (from-to)	30-65
Number of pages	36
Journal	Proceedings of the ACM on Programming Languages
Volume	9
Issue number	ICFP
DOIs	https://doi.org/10.1145/3747506
Publication status	Published - 5 Aug 2025

Keywords / Materials (for Non-textual outputs)

algebraic simplification
dependent types
free extension
frex
homomorphism
mathematically structured programming
universal algebra
universal property

Access to Document

10.1145/3747506Licence: Creative Commons: Attribution (CC-BY)

AllaisEtalPACMPL2025FrexDependentlyTypedFinal published version, 991 KBLicence: Creative Commons: Attribution (CC-BY)

Cite this

@article{c1a5e7c38cef4d83a1150ebf8a7f34c0,

title = "Frex: Dependently typed algebraic simplification",

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{\textquoteright}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 = "algebraic simplification, dependent types, free extension, frex, homomorphism, mathematically structured programming, universal algebra, universal property",

author = "Guillaume Allais and Edwin Brady and Nathan Corbyn and Ohad Kammar and Jeremy Yallop",

year = "2025",

month = aug,

day = "5",

doi = "10.1145/3747506",

language = "English",

volume = "9",

pages = "30--65",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery",

number = "ICFP",

}

TY - JOUR

T1 - Frex

T2 - Dependently typed algebraic simplification

AU - Allais, Guillaume

AU - Brady, Edwin

AU - Corbyn, Nathan

AU - Kammar, Ohad

AU - Yallop, Jeremy

PY - 2025/8/5

Y1 - 2025/8/5

N2 - 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.

AB - 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.

KW - algebraic simplification

KW - dependent types

KW - free extension

KW - frex

KW - homomorphism

KW - mathematically structured programming

KW - universal algebra

KW - universal property

UR - https://www.scopus.com/pages/publications/105012527322

U2 - 10.1145/3747506

DO - 10.1145/3747506

M3 - Article

AN - SCOPUS:105012527322

SN - 2475-1421

VL - 9

SP - 30

EP - 65

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - ICFP

M1 - 237

ER -

Frex: Dependently typed algebraic simplification

Abstract

Keywords / Materials (for Non-textual outputs)

Access to Document

Other files and links

Fingerprint

Cite this