Abstract of Paper

Abstract Syntax and Variable Binding for Linear Binders
by Miki Tanaka

Abstract:

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.