Directional types for logic programs and the annotation method

Abstract : A {\em directional type\/} for a Prolog program expresses certain properties of the operational semantics of the program. This paper shows that the annotation proof method, proposed by Deransart for proving declarative properties of logic programs, is also applicable for proving correctness of directional types. In particular, the sufficient correctness criterion of {\em well-typedness\/} by Bronsard et al, turns out to be a specialization of the annotation method. The comparison shows a general mechanism for construction of similar specializations, which is applied to derive yet another concept of well-typedness. The usefulness of the new correctness criterion is shown on examples of Prolog programs, where the traditional notion of well-typedness is not applicable. We further show that the new well-typing condition can be applied to different execution models. This is illustrated by an example of an execution model where unification is controlled by directional types, and where our new well-typing condition is applied to show the absence of deadlock.
Type de document :
[Research Report] RR-2471, INRIA. 1995
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:44:34
Dernière modification le : vendredi 16 septembre 2016 - 15:19:38
Document(s) archivé(s) le : lundi 5 avril 2010 - 00:06:46



  • HAL Id : inria-00074204, version 1



Johan Boye, Jan Maluszynski. Directional types for logic programs and the annotation method. [Research Report] RR-2471, INRIA. 1995. 〈inria-00074204〉



Consultations de la notice


Téléchargements de fichiers