Logic in Computer Science (LICS 1991)

Paper: Logic programs as types for logic programs (at LICS 1991)

Authors: Thom Fruhwirth Ehud Shapiro Moshe Y. Vardi Eyal Yardeni

Abstract

Optimistic type systems for logic programs are considered. In such systems types are conservative approximations to the success set of the program predicates. The use of logic programs to describe types is proposed. It is argued that this approach unifies the denotational and operational approaches to descriptive type systems and is simpler and more natural than previous approaches. The focus is on the use of unary-predicate programs to describe the types. A proper class of unary-predicate programs is identified, and it is shown that it is expensive enough to express several notions of types. An analogy with two-way automata and a correspondence with alternating algorithms are used to obtain a complexity characterization of type inference and type checking. This characterization is facilitated by the use of logic programs to represent types

BibTeX

  @InProceedings{FruhwirthShapiroVar-Logicprogramsastype,
    author = 	 {Thom Fruhwirth and Ehud Shapiro and Moshe Y. Vardi and Eyal Yardeni},
    title = 	 {Logic programs as types for logic programs},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1991},
    year =	 1991,
    editor =	 {Giles Kahn},
    month =	 {July}, 
    pages =      {300--309},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }