Logic in Computer Science (LICS 1999)

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 Symp. on Logic in Computer Science, {LICS} 1999},
    year =	 1999,
    editor =	 {Giuseppe Longo},
    month =	 {July}, 
    pages =      {454--463},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }