Substitution Without Copy and Paste

Thorsten Altenkirch, Nathaniel Burke, Philip Wadler

Defining substitution for a language with binders like the simply typed $\hat{I}»$-calculus requires repetition, defining substitution and renaming separately. To verify the categorical…