Partial objects in the calculus of constructions
- 10 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
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.Keywords
This publication has 4 references indexed in Scilit:
- Computational foundations of basic recursive function theoryPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Polymorphic rewriting conserves algebraic strong normalization and confluencePublished by Springer Nature ,1989
- The calculus of constructionsInformation and Computation, 1988
- Programming with proofs: A second order type theoryPublished by Springer Nature ,1988