Reference. A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory

William DeMeo, Jacques Carette · TYPES · 2022 · type-theory · DOI · arXiv
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.

Cite
Cite as @demeo-2022-a (helia, typst) · \cite{demeo-2022-a} (LaTeX)
BibTeX
bibtex · 14 lines
@inproceedings{demeo-2022-a,
  doi = {10.4230/LIPICS.TYPES.2021.4},
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.4},
  author = {DeMeo, William and Carette, Jacques},
  keywords = {Agda, constructive mathematics, dependent types, equational logic, formal verification, Martin-Löf type theory, model theory, universal algebra, Theory of computation → Logic and verification, Computing methodologies → Representation of mathematical objects, Theory of computation → Type theory},
  language = {en},
  title = {A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory},
  volume = {239},
  pages = {4:1-4:21},
  publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
  year = {2022},
  copyright = {Creative Commons Attribution 4.0 International license},
  booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}
}
hayagriva YAML (typst)
yaml · 16 lines
demeo-2022-a:
  type: article
  title: A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory
  author:
  - DeMeo, William
  - Carette, Jacques
  date: 2022
  page-range: 4:1-4:21
  url: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.4
  serial-number:
    doi: 10.4230/LIPICS.TYPES.2021.4
  parent:
    type: proceedings
    title: 27th International Conference on Types for Proofs and Programs (TYPES 2021)
    publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
    volume: 239
Download: demeo-2022-a.bib · demeo-2022-a.yml
Cited by (1)

Algebraic Effects Meet Hoare Logic in Cubical Agda kidney-2024-algebraicPOPL · 2024
This paper presents a novel formalisation of algebraic effects with equations in Cubical Agda. Unlike previous work in the literature that employed setoids to deal with equations, the library presented here uses quotient types to faithfully encode the type of terms quotiented by laws. Apart from tools for equational reasoning, the library also provides an effect-generic Hoare logic for algebraic effects, which enables reasoning about effectful programs in terms of their pre- and post-conditions. A particularly novel aspect is that equational reasoning and Hoare-style reasoning are related by an elimination principle of Hoare logic.
PDF · DOI · pldb
Cites 26 works (2 here)
With notes (2)

Formalizing category theory in Agda hu-2021-formalizingCPP · 2021
PDF · DOI · arXiv · pldb

Homotopy Type Theory: Univalent Foundations of Mathematics hottbookarXiv · 2013
Web · arXiv
External (24)
demeo-2022-a reference entries/refs/demeo-2022-a/demeo-2022-a.hel