Abstract de la publi numéro 4529

A new deciding algorithm of low polynomial complexity for categorical equivalence of derivations in intuitionistic multiplicative linear logic is described. It may be considered also as decision procedure for commutativity of diagrams of canonical natural transformations in symmetric monoidal closed categories.