Abstract
We consider a general prescriptive type system with parametricp olymorphism and subtyping for logic programs. The property of 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 logicp rograms 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.
A long version of this paper, containing all proofs, is available in [14].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
K. R. Apt. From Logic Programming to Prolog. Prentice Hall, 1997.
K. R. Apt and S. Etalle. On the unification free Prolog programs. In A. Borzyszkowski and S. Sokolowski, editors, Proceedings of MFCS, LNCS, pages 1–19. Springer-Verlag, 1993.
C. Beierle. Type inferencing for polymorphic order-sorted logic programs. In L. Sterling, editor, Proceedings of ICLP, pages 765–779. MIT Press, 1995.
R. Dietrich and F. Hagl. A polymorphic type system with subtypes for Prolog. In H. Ganzinger, editor, Proceedings of ESOP, LNCS, pages 79–93. Springer-Verlag, 1988.
F. Fages and M. Paltrinieri. A generict ype system for CLP(X). Technical report, Ecole Normale Supérieure LIENS 97-16, December 1997.
M. Hanus. Logic Programming with Type Specifications, chapter 3, pages 91–140. MIT Press, 1992. In [12].
P. M. Hill and J. W. Lloyd. The Gödel Programming Language. MIT Press, 1994.
P. M. Hill and R. W. Topor. A Semantics for Typed Logic Programs, chapter 1, pages 1–61. MIT Press, 1992. In [12].
T.K. Lakshman and U.S. Reddy. Typed Prolog: A semantic reconstruction of the Mycroft-O’Keefe type system. In V. Saraswat and K. Ueda, editors, Proceedings of ILPS, pages 202–217. MIT Press, 1991.
A. Mycroft and R. O’Keefe. A polymorphic type system for Prolog. Artificial Intelligence, 23:295–307, 1984.
G. Nadathur and F. Pfenning. Types in Higher-Order Logic Programming, chapter 9, pages 245–283. MIT Press, 1992. In [12].
F. Pfenning, editor. Types in Logic Programming. MIT Press, 1992.
J.-G. Smaus. Modes and Types in Logic Programming. PhD thesis, University of Kent at Canterbury, 1999.
J.-G. Smaus, F. Fages, and P. Deransart. Using modes to ensure subject reduction for typed logicp rograms with subtyping. Technical report, INRIA, 2000. Available via CoRR: http://arXiv.org/archive/cs/intro.html.
Z. Somogyi, F. Henderson, and T. Conway. The execution algorithm of Mercury, an efficient purely declarative logic programming language. Journal of Logic Programming, 29(1-3):17–64, 1996.
K. Stroetmann and T. Glaβ. A semantics for types in Prolog: The type system of pan version 2.0. Technical report, Siemens AG, ZFE T SE 1, 81730 München, Germany, 1995.
Simon Thompson. Type Theory and Functional Programming. Addison-Wesley, 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Smaus, JG., Fages, F., Deransart, P. (2000). Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping. In: Kapoor, S., Prasad, S. (eds) FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2000. Lecture Notes in Computer Science, vol 1974. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44450-5_17
Download citation
DOI: https://doi.org/10.1007/3-540-44450-5_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41413-1
Online ISBN: 978-3-540-44450-3
eBook Packages: Springer Book Archive