[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
Can some one tell me what is known about the decidability of the
equational theory on proof terms of the (tensor,I,!,-o)-fragment of
intuitionistic linear logic.
The equational theory I have in mind would be one that is sound and
complete for a particular class of models. The class of models I have
in mind are the L-NL models/Linear Categories although I'd also be
interested in the answer for other notions of model.
Also what applications would such a result have (if any!)?
Tel +33 1 44 32 32 77
Address LIENS-DMI, Ecole Normale Superieure,
45 Rue D'Ulm, 75230 Paris Cedex 05, France