Reference. Leveraging the Information Contained in Theory Presentations

A theorem prover without an extensive library is much less useful to its potential users. Algebra, the study of algebraic structures, is a core component of such libraries. Algebraic theories also are themselves structured, the study of which was started as Universal Algebra. Various constructions (homomorphism, term algebras, products, etc) and their properties are both universal and constructive. Thus they are ripe for being automated. Unfortunately, current practice still requires library builders to write these by hand. We first highlight specific redundancies in libraries of existing systems. Then we describe a framework for generating these derived concepts from theory definitions. We demonstrate the usefulness of this framework on a test library of 227 theories.

Cite

Cite as @carette-2020-leveraging (helia, typst) · \cite{carette-2020-leveraging} (LaTeX)
BibTeX
bibtex · 10 lines
@inproceedings{carette-2020-leveraging,
  author = {Jacques Carette and William M. Farmer and Yasmine Sharoda},
  title = {Leveraging the Information Contained in Theory Presentations},
  booktitle = {Intelligent Computer Mathematics},
  publisher = {Springer International Publishing},
  year = {2020},
  month = {7},
  pages = {55--70},
  doi = {10.1007/978-3-030-53518-6_4}
}
hayagriva YAML (typst)
yaml · 15 lines
carette-2020-leveraging:
  type: article
  title: Leveraging the Information Contained in Theory Presentations
  author:
  - Carette, Jacques
  - Farmer, William M.
  - Sharoda, Yasmine
  date: 2020-07
  page-range: 55-70
  serial-number:
    doi: 10.1007/978-3-030-53518-6_4
  parent:
    type: proceedings
    title: Intelligent Computer Mathematics
    publisher: Springer International Publishing
Cited by (1)

Frex: Dependently Typed Algebraic Simplification allais-2025-frex

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.
PDF · DOI · pldb
Cites 35 works (1 here)
With notes (1)

Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages carette-2009-finally

We have built the first family of tagless interpretations for a higher-order typed object language in a typed metalanguage (Haskell or ML) that require no dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value continuation-passing style (CPS) transformers. Our principal technique is to encode de Bruijn or higher-order abstract syntax using combinator functions rather than data constructors. In other words, we represent object terms not in an initial algebra but using the coalgebraic structure of the λ-calculus. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations. Our encoding of an object term abstracts uniformly over the family of ways to interpret it, yet statically assures that the interpreters never get stuck. This family of interpreters thus demonstrates again that it is useful to abstract over higher-kinded types.
PDF · DOI · pldb
External (34)
carette-2020-leveraging reference entries/refs/carette-2020-leveraging/carette-2020-leveraging.hel