Logic in Computer Science (LICS 1991)

Paper: Toward a semantics for the QUEST language (at LICS 1991)

Authors: Fabio Alessi Franco Barbanera

Abstract

A model is given for the second-order lambda calculus extended with inheritance, bounded quantification, recursive types, constructors and kinds. This language, called μ-FunK, can be viewed as the core of the QUEST language defined by L. Cardelli (SRC Rep. 45, 1989). Types are interpreted as intervals of partial equivalence relations. Because of the properties of intervals and their ordering, all the type constructors are continuous functions. As a consequence a system where a kind is given to each constructor constant employed can be modeled. In such a model the meaning of operator μ, the constructor of recursive types, turns out to be just the minimal fixed-point operator

BibTeX

  @InProceedings{AlessiBarbanera-Towardasemanticsfor,
    author = 	 {Fabio Alessi and Franco Barbanera},
    title = 	 {Toward a semantics for the QUEST language},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1991},
    year =	 1991,
    editor =	 {Giles Kahn},
    month =	 {July}, 
    pages =      {12--21},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }