Logic in Computer Science (LICS 1991)

Paper: A first-order theory of types and polymorphism in logic programming (at LICS 1991)

Authors: Michael Kifer James Wu

Abstract

A logic called typed predicate calculus (TPC) that gives declarative meaning to logic programs with type declarations and type inference is introduced. The proper interaction between parametric and inclusion varieties of polymorphism is achieved through a construct called type dependency, which is analogous to implication types but yields more natural and succinct specifications. Unlike other proposals where typing has extra-logical status, in TPC the notion of type-correctness has precise model-theoretic meaning that is independent of any specific type-checking or type-inference procedure. Moreover, many different approaches to typing that were proposed in the past can be studied and compared within the framework of TPC. Another novel feature of TPC is its reflexivity with respect to type declarations; in TPC, these declarations can be queried the same way as any other data. Type reflexivity is useful for browsing knowledge bases and, potentially, for debugging logic programs

BibTeX

  @InProceedings{KiferWu-Afirstordertheoryof,
    author = 	 {Michael Kifer and James Wu},
    title = 	 {A first-order theory of types and polymorphism in logic programming },
    booktitle =  {Proceedings of the Sixth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1991},
    year =	 1991,
    editor =	 {Giles Kahn},
    month =	 {July}, 
    pages =      {310--321},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }