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

Authors: 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}
  }