License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2021.4
URN: urn:nbn:de:0030-drops-167737
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16773/
DeMeo, William ;
Carette, Jacques
A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory
Abstract
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.
BibTeX - Entry
@InProceedings{demeo_et_al:LIPIcs.TYPES.2021.4,
author = {DeMeo, William and Carette, Jacques},
title = {{A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-L\"{o}f Type Theory}},
booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages = {4:1--4:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-254-9},
ISSN = {1868-8969},
year = {2022},
volume = {239},
editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16773},
URN = {urn:nbn:de:0030-drops-167737},
doi = {10.4230/LIPIcs.TYPES.2021.4},
annote = {Keywords: Agda, constructive mathematics, dependent types, equational logic, formal verification, Martin-L\"{o}f type theory, model theory, universal algebra}
}
