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

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00072621
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:24:54 AM
Last modification on : Friday, May 25, 2018 - 12:02:03 PM
Long-term archiving on : Sunday, April 4, 2010 - 11:15:42 PM

Identifiers

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

Share

Metrics

Record views

162

Files downloads

208