School of Computing

Backward Type Inference Generalises Type Checking

L. Lu and A. King

In M. Hermenegildo and G. Puebla, editors, Ninth International Static Analysis Symposium, volume 2477 of Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, September 2002 Also see http://www.springer.de/comp/lncs/index.html.

Abstract

This paper presents a backward type analysis for logic programs. Given type signatures for a collection of selected predicates such as builtin or library predicates, the analysis infers type signatures for other predicates such that the execution of any query satisfying the inferred type signatures will not violate the type signatures for the selected predicates. Thus, the backward type analysis generalises type checking in which the programmer manually specifies type signatures for all predicates that are checked for consistency by a type checker.

Download publication 1722 kbytes (PostScript)

Bibtex Record

@inproceedings{1389,
author = {L.~Lu and A.~King},
title = {Backward {T}ype {I}nference {G}eneralises {T}ype {C}hecking},
month = {September},
year = {2002},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {Also see http://www.springer.de/comp/lncs/index.html},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2002/1389},
    publication_type = {inproceedings},
    submission_id = {12806_1025511174},
    booktitle = {Ninth International Static Analysis Symposium},
    series = {Lecture Notes in Computer Science},
    publisher = {Springer-Verlag},
    refereed = {yes},
    volume = {2477},
    editor = {M. Hermenegildo and G. Puebla},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014