2023/06/27 by Guillaume Allais, Allais, Guillaume, Edwin Brady +7 · 1 citation
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Programming Languages (cs.PL) #Software Engineering Research #Symbolic Computation (cs.SC)
paper · pdf · doi:10.48550/arxiv.2306.15375
openalex publication_date 2023/06/27 · openalex created_date 2023/06/29 · openalex updated_date 2026/07/28
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.