Semantics Club 17 11 2000
This talk gives a theory for modelling binders with a linearity condition, using presheaf categories. This study can be regarded as a linear version of the paper by Fiore et al. 1999, which deals with ordinary binders.
In order to model linearity, we employ symmetric monoidal structure for modelling contexts, in place of finite product structure used in the ordinary case. This change is reflected in the various operators constructed on this model of contexts so that these operators give linearity as desired.