Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping

Abstract : We consider a general prescriptive type system with parametric polymorphism and subtyping for logic programs. The property of \em subject reduction expresses the consistency of the type system w.r.t.\ the execution model: if a program is «well-typed», then all derivations starting in a «well-typed» goal are again «well-typed». It is well-established that without subtyping, this property is readily obtained for logic programs w.r.t. their standard (untyped) execution model. Here we give syntactic conditions that ensure subject reduction also in the presence of general subtyping relations between type constructors. The idea is to consider logic programs with a fixed dataflow, given by modes.
Type de document :
Rapport
[Research Report] RR-4020, INRIA. 2000
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00072621
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 10:24:54
Dernière modification le : samedi 17 septembre 2016 - 01:29:46
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:15:42

Fichiers

Identifiants

  • HAL Id : inria-00072621, version 1

Collections

Citation

Jan-Georg Smaus, Francois Fages, Pierre Deransart. Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping. [Research Report] RR-4020, INRIA. 2000. 〈inria-00072621〉

Partager

Métriques

Consultations de la notice

136

Téléchargements de fichiers

143