Sixth Annual IEEE Symposium on

Logic in Computer Science (LICS 1991)

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

Authors: Philippe Audebaud


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


    author = 	 {Philippe Audebaud},
    title = 	 {Partial objects in the calculus of constructions},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1991},
    year =	 1991,
    editor =	 {Giles Kahn},
    month =	 {July}, 
    pages =      {86--95},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}