Logic in Computer Science (LICS 1989)

Paper: Unified algebras and institutions (at LICS 1989)

Authors: Mosses, P.D.

Abstract

A framework for algebraic specification of abstract data types is introduced. It involves so-called unified algebras, where sorts are treated as values, so that operations can be applied to sorts as well as to the elements that they classify. An institution for unified algebras is defined and shown to be liberal. However, the ordinary forgetful functor does not forget any values in unified algebras, so the usual data constraints do not have any models. A more forgetful functor is introduced and used to define so-called bounded data constraints, which have the expected models

BibTeX

  @InProceedings{Mosses-Unifiedalgebrasandi,
    author = 	 {Mosses, P.D.},
    title = 	 {Unified algebras and institutions},
    booktitle =  {Proceedings of the Fourth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1989},
    year =	 1989,
    editor =	 {Rohit Parikh},
    month =	 {June}, 
    pages =      {304--312},
    location =   {Pacific Grove, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }