Efficient run-time type checking of typed logic programs

Abstract

This paper presents a new approach to the problem of guaranteeing that definite logic programs are free of type errors. Previously, two approaches to this problem have been considered. The first approach is static type checking, in which predicate types are inferred from the program and checked for self-consistency and for consistency with declared types. Static type checking, however, is in general incomplete, as it can neither only reject programs with type errors nor only accept programs which are type-error free. The second approach is dynamic type checking, in which types are checked against type declarations at run-time. Dynamic type checking, however, is prohibitively expensive. Our a..