Logic in Computer Science (LICS 1988)

Paper: A categorical semantics of constructions (at LICS 1988)

Authors: Thomas Ehrhard

Abstract

An abstract framework is proposed for the description of the type dependency semantics. It is claimed that the notion of fibration introduced by A. Grothendieck in the 1960s is perfectly adapted to this goal and provides the greatest simplicity and generality. This semantics is extended to higher order, and an explanation is given of what a general definition for the semantics of the theory of constructions could be

BibTeX

  @InProceedings{Ehrhard-Acategoricalsemanti,
    author = 	 {Thomas Ehrhard},
    title = 	 {A categorical semantics of constructions},
    booktitle =  {Proceedings of the Third Annual IEEE Symp. on Logic in Computer Science, {LICS} 1988},
    year =	 1988,
    editor =	 {Yuri Gurevich},
    month =	 {July}, 
    pages =      {264--273},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }