Go to the corresponding LIPIcs Volume Portal 
DeMeo, William ; Carette, Jacques
pdfformat: 

@InProceedings{demeo_et_al:LIPIcs.TYPES.2021.4, author = {DeMeo, William and Carette, Jacques}, title = {{A MachineChecked Proof of Birkhoff’s Variety Theorem in MartinL\"{o}f Type Theory}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {4:14:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {9783959772549}, ISSN = {18688969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16773}, URN = {urn:nbn:de:0030drops167737}, doi = {10.4230/LIPIcs.TYPES.2021.4}, annote = {Keywords: Agda, constructive mathematics, dependent types, equational logic, formal verification, MartinL\"{o}f type theory, model theory, universal algebra} }
Keywords:  Agda, constructive mathematics, dependent types, equational logic, formal verification, MartinLöf type theory, model theory, universal algebra  
Collection:  27th International Conference on Types for Proofs and Programs (TYPES 2021)  
Issue Date:  2022  
Date of publication:  04.08.2022  
Supplementary Material:  Software (Agda Sources): https://github.com/ualib/agdaalgebras archived at: https://archive.softwareheritage.org/swh:1:dir:29817e5c87bb55467269dad672f7f4b4152733d7 