This is an unofficial reimagining of the Archive of Formal Proofs
A General Theory of Syntax with Bindingsby Lorenzo Gheri and Andrei Popescu