Logic in Computer Science (LICS 1989)

Paper: Structure and representation in LF (at LICS 1989)

Authors: Harper, R. Sannella, D. Tarlecki, A.

Abstract

An important tool for controlling search in an object logic is the use of structured theory presentations. In order to apply these ideas to the setting of a logical framework, the authors study the behavior of structured theory presentations under representation in a framework, focusing on the problem of lifting presentations, from the object logic to the metalogic of the framework. The authors also consider imposing structure on logic presentations so that logical systems may themselves be defined in a modular fashion. This opens the way to a CLEAR-like language for defining both theories and logics in a logical framework

BibTeX

  @InProceedings{HarperSannellaTarle-Structureandreprese,
    author = 	 {Harper, R. and Sannella, D. and Tarlecki, A.},
    title = 	 {Structure and representation in LF},
    booktitle =  {Proceedings of the Fourth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1989},
    year =	 1989,
    editor =	 {Rohit Parikh},
    month =	 {June}, 
    pages =      {226--237},
    location =   {Pacific Grove, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }