Optimal multi-binding unification for sharing and linearity analysis

Abstract

In the analysis of logic programs, abstract domains for detecting sharing properties are widely used. Recently the new domain $\Linp$ has been introduced to generalize both sharing and linearity information. This domain is endowed with an optimal abstract operator 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.

To appear in Theory and Practice of Logic Programming (TPLP)

References in corpus (2)

• Optimality in Goal-Dependent Analysis of Sharing
• On the interaction between sharing and linearity

Cited by in corpus (1)

• Optimal matching for sharing and linearity analysis