Semantics Club 17 11 2000

Abstract Syntax and Variable Binding for Linear Binders

Miki Tanaka


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.