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	Issue ICFP
Early online date	5 Aug 2025
DOIs	https://doi.org/10.1145/3747506
Publication status	Published - Aug 2025

Keywords

Dependent types
Frex
Free extension
Mathematically structured programming
Universal algebra
Algebraic simplification
Homomorphism
Universal property

Access to Document

10.1145/3747506Licence: CC BY

Allais-et-al-2025-Frex-dependently-typed-ProcACMProgLang-9-ICFP-30-CCBY
Copyright © 2025 Owner/Author. This work is licensed under Creative Commons Attribution International 4.0.
Final published version, 916 KBLicence: CC BY

Cite this

@article{93caf57b364c49acb5c7d17ac242f36e,

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'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 = "Dependent types, Frex, Free extension, Mathematically structured programming, Universal algebra, Algebraic simplification, Homomorphism, Universal property",

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

note = "Funding: Supported by the Engineering and Physical Sciences Research Council grant EP/T007265/1 and an Industrial CASE Studentship, a Royal Society University Research Fellowship, a Facebook Research Award, an Alan Turing Institute seed-funding grant, and UK Advanced Research and Innovation Agency (ARIA) as part of the project Qbs4Safety: Core Representation Underlying Safeguarded AI.",

year = "2025",

month = aug,

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 = "Issue ICFP",

}

TY - JOUR

T1 - Frex: dependently typed algebraic simplification

AU - Allais, Guillaume

AU - Brady, Edwin

AU - Corbyn, Nathan

AU - Kammar, Ohad

AU - Yallop, Jeremy

N1 - Funding: Supported by the Engineering and Physical Sciences Research Council grant EP/T007265/1 and an Industrial CASE Studentship, a Royal Society University Research Fellowship, a Facebook Research Award, an Alan Turing Institute seed-funding grant, and UK Advanced Research and Innovation Agency (ARIA) as part of the project Qbs4Safety: Core Representation Underlying Safeguarded AI.

PY - 2025/8

Y1 - 2025/8

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 - Dependent types

KW - Frex

KW - Free extension

KW - Mathematically structured programming

KW - Universal algebra

KW - Algebraic simplification

KW - Homomorphism

KW - Universal property

U2 - 10.1145/3747506

DO - 10.1145/3747506

M3 - Article

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 - Issue ICFP

M1 - 237

ER -

Frex: dependently typed algebraic simplification

Abstract

Keywords

Access to Document

Fingerprint

Cite this