@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)}
}