This is an unofficial reimagining of the Archive of Formal Proofs
Formalizing the Logic-Automaton Connectionby Stefan Berghofer and Markus Reiter