**Next:**Pingali

**Up:**Results from Prior

**Previous:**Results from Prior

## Constable

Most of the basic science and software design of Cornell's computational type theory was supported with NSF funding to R. L. Constable joined by various colleagues, principally J. Bates in the 80's and D. Howe in the 90's. The same investigators led the implementation of this theory in Nuprl, funded by NSF. The DoD (ONR and ARO), NASA and industry (IBM, Intel, Xerox, and AT&T) have funded applications in hardware and software verification.

This section will summarize some of the most relevant recent work. Many of the basic ideas we have introduced are explained in books written by others on programming languages [109,99] or on knowledge representation [110] or on automated reasoning [51,78].

The computational type theory of Nuprl is closely related to Per
Martin-Löf's * Intuitionistic Type Theory* [76], but
differs in significant ways in order to provide a foundation for
computer science as well as mathematics; it is also closely related to
work done at Cornell on * programming logics* [28]. For
example, Nuprl uses recursive data types inspired by domain theory
[101] rather than Martin-Löf's W-types (well-founded
types), and it introduced * set types* [25] in order
to model certain kinds of partial functions and * quotient types*
to allow information hiding.

Another substantial departure from Martin-Löf theories is the use
of so-called * direct computation rules* which allow untyped
computation on terms during the process of demonstrating that they are
well-formed. This enables Nuprl to use general recursive function
definitions as in functional programming languages --- untyped ML
programs are essentially a sublanguage of Nuprl.

Recent work provided a reflection mechanism for Nuprl. This required
a semantic account of proofs [4] and new primitive data
types (such as OpNames). The new base types allowed us to define
internal types Term and Proof to represent the Nuprl definitions *
term* and * proof*.

Recently [8,3] Constable has explored the notion of a higher-order abstract data type (ADT). This concept relies on the encoding of higher order logic types (via propositions-as-types) so that induction principles can be packaged with the data operators. This mechanism has been used to solve the problem of safely adding decision procedures to tactic-based theorem provers [3].

**Next:**Pingali

**Up:**Results from Prior

**Previous:**Results from Prior

*nuprl project*

Tue Nov 21 08:50:14 EST 1995

Tue Nov 21 08:50:14 EST 1995