Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00074204
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 2:44:34 PM
Last modification on : Thursday, February 11, 2021 - 2:50:07 PM
Long-term archiving on: : Monday, April 5, 2010 - 12:06:46 AM

Identifiers

  • HAL Id : inria-00074204, version 1

Collections

Citation

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

Share

Metrics

Record views

125

Files downloads

92