## Paper: Correctness of Multiplicative Proof Nets is Linear (at LICS 1999)

**Stefano Guerrini**

### Abstract

We reformulate Danos contractibility criterion in terms of a sort of unification. As for term unification, a direct implementation of the unification criterion leads to a quasi-linear algorithm. Linearity is obtained after observing that the disjoint-set union-find at the core of the unification criterion is a special case of union-find with a real linear time solution.

### BibTeX

@InProceedings{Guerrini-CorrectnessofMultip, author = {Stefano Guerrini}, title = {Correctness of Multiplicative Proof Nets is Linear}, booktitle = {Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1999)}, year = {1999}, month = {July}, pages = {454--463}, location = {Trento, Italy}, publisher = {IEEE Computer Society Press} }