eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-08-04
4:1
4:21
10.4230/LIPIcs.TYPES.2021.4
article
A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory
DeMeo, William
1
https://orcid.org/0000-0003-1832-5690
Carette, Jacques
2
https://orcid.org/0000-0001-8993-9804
New Jersey Institute of Technology, Newark, NJ, USA
McMaster University, Hamilton, Canada
The Agda Universal Algebra Library is a project aimed at formalizing the foundations of universal algebra, equational logic and model theory in dependent type theory using Agda. In this paper we draw from many components of the library to present a self-contained, formal, constructive proof of Birkhoff’s HSP theorem in Martin-Löf dependent type theory. This achieves one of the project’s initial goals: to demonstrate the expressive power of inductive and dependent types for representing and reasoning about general algebraic and relational structures by using them to formalize a significant theorem in the field.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol239-types2021/LIPIcs.TYPES.2021.4/LIPIcs.TYPES.2021.4.pdf
Agda
constructive mathematics
dependent types
equational logic
formal verification
Martin-Löf type theory
model theory
universal algebra