Abstract interpretation for type checking

Abstract

The typed logic languages are more expressive than the usual untyped ones, but run-time type-checking is in general quite costly. Compile-time type checking is a classical application of the abstract interpretation paradigm. We describe a general abstract interpretation framework and inside it we develop two new methods for the compile-time type-checking of typed logic programs. The first method applies to a restricted class of programs (those that are type-preserving and use a finite number of types) and it detects the programs that need no type-checking at all. The second one applies to any program, but, in general, it only avoids part of the run-time type-checking.