Hostname: page-component-78c5997874-xbtfd Total loading time: 0 Render date: 2024-11-09T05:55:27.126Z Has data issue: false hasContentIssue false

Typing constraint logic programs

Published online by Cambridge University Press:  09 June 2004

FRANÇOIS FAGES
Affiliation:
Projet Contraintes, INRIA-Rocquencourt, BP105, 78153 Le Chesnay Cedex, France, (e-mail: [email protected], [email protected])
EMMANUEL COQUERY
Affiliation:
Projet Contraintes, INRIA-Rocquencourt, BP105, 78153 Le Chesnay Cedex, France, (e-mail: [email protected], [email protected])

Abstract

We present a prescriptive type system with parametric polymorphism and subtyping for constraint logic programs. The aim of this type system is to detect programming errors statically. It introduces a type discipline for constraint logic programs and modules, while maintaining the capabilities of performing the usual coercions between constraint domains, and of typing meta-programming predicates, thanks to the exibility of subtyping. The property of subject reduction expresses the consistency of a prescriptive type system w.r.t. the execution model: if a program is ‘well-typed’, then all derivations starting from a ‘well-typed’ goal are again ‘well-typed’. That property is proved w.r.t. the abstract execution model of constraint programming which proceeds by accumulation of constraints only, and w.r.t. an enriched execution model with type constraints for substitutions. We describe our implementation of the system for type checking and type inference. We report our experimental results on type checking ISO-Prolog, the (constraint) libraries of Sicstus Prolog and other Prolog programs.

Type
Research Article
Copyright
© 2001 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)