Paper: Infinite Objects in Type Theory (at LICS 1986)

Authors: Nax P. Mendler Prakash Panangaden Robert L. Constable

Abstract

In this paper we show how infinite objects can be defined in a constructive type theory. The type theory that we use is variant of Martin-Lof's Intuitionistic Type Theory. We show how one can express the intuition that infinite objects are understood through a limiting process without having to introduce partial objects in the theory. This means that we can adhere to the propositions-as-types principle. The type of infinite objects thus contains only total elements. The approximation is expressed through a sequence of types that approximate the type of infinte objects. We give two semantic accounts of types of infinite objects. The first is lattice theoretic and shows how these types can be understood as fixed points. The second is category theoretic and shows the duality between types of infinte objects and the ordinary recursive type definitions.

BibTeX

  @InProceedings{MendlerPanangadenCo-InfiniteObjectsinTy,
    author = 	 {Nax P. Mendler and Prakash Panangaden and Robert L. Constable},
    title = 	 {Infinite Objects in Type Theory},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {249--255},
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }