We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: A Machine-checked proof of Birkhoff's Variety Theorem in Martin-Löf Type Theory

Abstract: The Agda Universal Algebra Library (agda-algebras) is a library of types and programs (theorems and proofs) we developed to formalize the foundations of universal algebra in dependent type theory using the Agda programming language and proof assistant. In this paper we draw on and explain many components of the agda-algebras library, which we extract into a single Agda module in order to present a self-contained formal and constructive proof of Birkhoff's HSP theorem in Martin-L\"of dependent type theory. In the course of our presentation, we highlight some of the more challenging aspects of formalizing the basic definitions and theorems of universal algebra in type theory. Nonetheless, we hope this paper and the agda-algebras library serve as further evidence in support of the claim that dependent type theory and the Agda language, despite the technical demands they place on the user, are accessible to working mathematicians (such as ourselves) who possess sufficient patience and resolve to formally verify their results with a proof assistant. Indeed, the agda-algebras library now includes a substantial collection of definitions, theorems, and proofs from universal algebra, illustrating the expressive power of inductive and dependent types for representing and reasoning about general algebraic and relational structures.
Comments: This is the long (35 page) version of a paper submitted to TYPES 2021; the previous draft, [v2], was a comprehensive description of an old version of the Agda Universal Algebra Library (called UALib; ver. 1.0.0); the library was rewritten and renamed agda-algebras (ver. 2.0.0); this paper describes only a subset of the agda-algebras library that we used to prove Birkhoff's HSP theorem in Agda
Subjects: Logic in Computer Science (cs.LO); Logic (math.LO)
MSC classes: 68V20 (Primary) 03C05 (Secondary)
ACM classes: F.4.1
Cite as: arXiv:2101.10166 [cs.LO]
  (or arXiv:2101.10166v3 [cs.LO] for this version)

Submission history

From: William DeMeo [view email]
[v1] Mon, 25 Jan 2021 15:26:58 GMT (687kb)
[v2] Fri, 5 Feb 2021 23:02:10 GMT (733kb)
[v3] Tue, 30 Nov 2021 22:13:47 GMT (293kb,D)

Link back to: arXiv, form interface, contact.