Under consideration for publication in Theory and Practice of Logic Programming 1 Optimal multi-binding unification for sharing and linearity analysis

In the analysis of logic programs, abstract domains for detecting sharing properties are widely used. Recently the new domain ShLinω has been introduced to generalize both sharing and linearity information. This domain is endowed with an optimal abstract oper-ator for single-binding unification. The authors claim that the repeated application of this operator is also optimal for multi-binding unification. This is the proof of such a claim