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

Jan-Georg Smaus, François Fages, Pierre Deransart

To appear at Foundations of Software Technology and Theoretical Computer Science (FSTTCS2000), New Delhi, India, December 13-15 2000


We consider prescriptive type systems with subtyping for logic programs. One desirable property of a prescriptive type system is thatthe typing is static: if a program is ``well-typed'', then all derivations starting in a ``well-typed'' goal are again ``well-typed'', and so types can be ignored at runtime (subject reduction). It is well-established that without subtyping, this property is readily obtained. We study conditions which ensure subject reduction also in the presence of general subtyping relations between type constructors. The idea is to give a fixed dataflow to a logic program by introducing modes.

Server START Conference Manager
Update Time 14 Aug 2000 at 17:41:23
Start Conference Manager
Conference Systems