Paper: Partial objects in the calculus of constructions (at LICS 1991)

Authors: Philippe Audebaud

Abstract

A typed framework for working with nonterminating computations is provided. The basic system is the calculus of constructions. It is extended using an original idea proposed by R. Constable and S.F. Smith (2nd Ann. IEEE Conf. on Logic in Comput. Sci., 1987) and implemented in Nuprl. From the computational point of view, an equivalent of the Kleene theorem for partial recursive functions over the integers within an index-free setting is obtained. A larger class of algebraic types is defined. Logical aspects need more examination, but a syntactic method for dealing with partial and total objects, leading to the notion of generic proof, is provided

BibTeX

  @InProceedings{Audebaud-Partialobjectsinthe,
    author = 	 {Philippe Audebaud},
    title = 	 {Partial objects in the calculus of constructions},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991)},
    year =	 {1991},
    month =	 {July}, 
    pages =      {86--95},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }