|Abstract of Paper|
Abstract Syntax and Variable Binding for Linear Binders
by Miki Tanaka
We apply the theory of binding algebra to syntax with linear binders. We construct a category of models for a linear binding signature. The initial model serves as abstract syntax for the signature. Moreover it contains structure for modelling simultaneous substitution. We use the presheaf category on the free symmetric monoidal category on 1 to construct models of each binding signature.