HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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 :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 2:44:34 PM
Last modification on : Friday, February 4, 2022 - 3:16:30 AM
Long-term archiving on: : Monday, April 5, 2010 - 12:06:46 AM


  • 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⟩



Record views


Files downloads