Frex: dependently-typed algebraic simplification
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2023
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866912489595207680 |
|---|---|
| author | Allais, Guillaume Brady, Edwin Corbyn, Nathan Kammar, Ohad Yallop, Jeremy |
| author_facet | Allais, Guillaume Brady, Edwin Corbyn, Nathan Kammar, Ohad Yallop, Jeremy |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2306_15375 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Frex: dependently-typed algebraic simplification Allais, Guillaume Brady, Edwin Corbyn, Nathan Kammar, Ohad Yallop, Jeremy Programming Languages Logic in Computer Science Symbolic Computation 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. |
| title | Frex: dependently-typed algebraic simplification |
| topic | Programming Languages Logic in Computer Science Symbolic Computation |
| url | https://arxiv.org/abs/2306.15375 |