collaborators

1 paper

cs.LO2021

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

William DeMeo, Jacques Carette

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 depend…