Intuitionistic implication in abstract interpretation

Abstract

In this paper we introduce the notion of Heyting completion in abstract interpretation, and we prove that it supplies a logical basis to specify relational program analyses by means of intuitionistic implication. This provides a uniform algebraic setting where abstract domains can be specified by simple logic formulas, or as solutions of recursive abstract domain equations, involving few basic operations for domain construction. We apply our framework to study directionality in type inference and groundness analysis in logic programming.