Oxford Journals
tools journals homepage advanced search contact help
Journal of Logic and Computation: Current Issue
 
home
browse
current
etoc
authors
subinfo
subscribers
samples

OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation

Journal of Logic and Computation

Volume 12, Issue 3, June 2002: pp. 497-542

Generalizing Def and Pos to Type Analysis

Patricia M. Hill1 and Fausto Spoto2

1School of Computing, University of Leeds, Leeds, LS2 9JT, UK. E-mail: hill@comp.leeds.ac.uk
2Dipartimento Scientifico e Tecnologico, Strada Le Grazie, 15, 37134 Verona, Italy. E-mail: spoto@sci.univr.it

This paper is concerned with the type analysis of logic programs where, by type, we mean a property closed under instantiation. We define a chain of abstractions from Herbrand constraints to logical formulas via the set of their solutions. Every step of the chain is an instance of abstract interpretation. The use of logical formulas for type analysis is a generalization of the traditional Boolean domains Def and Pos for groundness analysis. In this context, implication is the logical counterpart of the use of linear refinement. While logical formulas can sometime be used for an actual implementation of our domains, in the general case they are infinite objects. Therefore, we apply a final abstraction from possibly infinite logical formulas to (finite) logic programs. Thus, logic programs are themselves used for the type analysis of logic programs. The advantage of our technique with respect to the many frameworks for type analysis present in the literature is that we have developed our domains by using the formal techniques of abstract interpretation and linear refinement. Therefore, their construction is guided by the underlying theory, from which their properties are derived.

Keywords: Abstract interpretation; domain theory; linear refinement; type theory; type analysis; logic programming

Table of Contents   Full-Text PDF (598 KB)

Oxford University Press
Published by Oxford University Press
Copyright ©Oxford University Press 2003
Print ISSN: 0955-792X  Online ISSN: 1465-363X.
Oxford University Press Privacy Policy and Legal Statement