References. A New Approach to Abstract Syntax Involving Binders (Gabbay, Pitts, 1999) A New Approach to Abstract Syntax with Variable Binding (Gabbay, Pitts, 2002) Alpha Equivalence Equalities (Crole, 2012) Categorical Logic (Shulman, 2016)