Substitution Without Copy and Paste

Thorsten Altenkirch, Nathaniel Burke, Philip Wadler

Defining substitution for a language with binders like the simply typed $\lambda$-calculus requires repetition, defining substitution and renaming separately. To verify the categorical p…