Formalizing universal algebra with dependent and inductive types

JMM Special Session on Algebras and Algorithms

William DeMeo

Denver, Colorado, Wed 15 Jan 2020

(For the latest updates, please visit ualib.org.)

• 1. Preface
  • 1.1. Vision
  • 1.2. Objectives
  • 1.3. Intended audience
  • 1.4. Installing the library
  • 1.5. Acknowledgments
  • 1.6. References
• 2. Datatypes for Algebras
  • 2.1. Preliminaries
  • 2.2. Signatures
  • 2.3. Operations
  • 2.4. Algebras
  • 2.5. Homomorphisms
• 3. Datatypes for Terms
  • 3.1. Terms
  • 3.2. The term algebra
  • 3.3. The universal property
• 4. Datatypes for Subuniverses and Subalgebras
  • 4.1. Subuniverses
  • 4.2. Subalgebras

Appendix

• Note on axiom K
• Writing definitions interactively
• REFERENCES

Please email comments, suggestions, and corrections to williamdemeo@gmail.com