More Precise Yet Efficient Type Inference for Logic Programs

TL;DR

This paper introduces a more precise and efficient type inference method for logic programs using an abstract interpretation framework, improving the widening operator and demonstrating practical benefits.

Contribution

It proposes a novel widening operator that enhances precision without sacrificing efficiency in type analysis of logic programs.

Findings

The new widening operator improves analysis precision.

The analysis domain enables efficient type inference.

Practical results show effectiveness in real-world scenarios.

Abstract

Type analyses of logic programs which aim at inferring the types of the program being analyzed are presented in a unified abstract interpretation-based framework. This covers most classical abstract interpretation-based type analyzers for logic programs, built on either top-down or bottom-up interpretation of the program. In this setting, we discuss the widening operator, arguably a crucial one. We present a new widening which is more precise than those previously proposed. Practical results with our analysis domain are also presented, showing that it also allows for efficient analysis.