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].