Collection analysis for Horn clause programs

Dale Miller 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : We consider approximating data structures with collections of the items that they contain. For examples, lists, binary trees, tuples, etc, can be approximated by sets or multisets of the items within them. Such approximations can be used to provide partial correctness properties of logic programs. For example, one might wish to specify than whenever the atom $sort(t,s)$ is proved then the two lists $t$ and $s$ contain the same multiset of items (that is, $s$ is a permutation of $t$). If sorting removes duplicates, then one would like to infer that the sets of items underlying $t$ and $s$ are the same. Such results could be useful to have if they can be determined statically and automatically. We present a scheme by which such collection analysis can be structured and automated. Central to this scheme is the use of linear logic as a omputational logic underlying the logic of Horn clauses.
Type de document :
Communication dans un congrès
International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Jul 2006, Venice, Italy
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00167225
Contributeur : Dale Miller <>
Soumis le : jeudi 16 août 2007 - 17:43:00
Dernière modification le : jeudi 10 mai 2018 - 02:06:40
Document(s) archivé(s) le : vendredi 9 avril 2010 - 00:50:14

Fichiers

ppdp06-hal.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

  • HAL Id : inria-00167225, version 1
  • ARXIV : 0708.2230

Collections

Citation

Dale Miller. Collection analysis for Horn clause programs. International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Jul 2006, Venice, Italy. 〈inria-00167225〉

Partager

Métriques

Consultations de la notice

263

Téléchargements de fichiers

114