Pith. sign in

REVIEW 1 cited by

Frex: dependently-typed algebraic simplification

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2306.15375 v2 pith:RNNX6IJL submitted 2023-06-27 cs.PL cs.LOcs.SC

Guillaume Allais , Edwin Brady , Nathan Corbyn , Ohad Kammar , Jeremy Yallop This is my paper
classification cs.PLcs.LOcs.SC
keywords simplificationalgebraicalgebrasdependentlydesignextractionfreelibrary
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original 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.

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Custom Representations of Inductive Families

    cs.PL 2025-05 conditional novelty 7.0 of 10 partial

    Custom representations of inductive families, formalized as inductive algebras with a Repr modality, erase representation-conversion overhead during compilation.

Pith tools