Our project grew out of work on programming logics that has its origins in John McCarthy's outline of a theory of computing in which he presented a logic for reasoning about Lisp.
Essentially our work in logic started with the observation in 1971 that constructive proofs could be interpreted as programs. Constable saw this idea as the basis for a programming logic, but he wanted the programs to be ordinary imperative programs of the kind the CS Department was teaching in courses. So he worked out the idea that certain "safe" PL/I programs could be thought of as the computational skeletons of constructive proofs. At the time there was a project in the CS Department to create a disciplined subset of PLI for which a formal semantics and a programming logic could be built. The subset was called PL/CS and the verifier was PL/CV. The logic that he and Mike O'Donnell built around it was a new kind of programming logic in which proofs could include programming commands. These proofs could also be seen as asserted programs.
As we tried to extend this logic to account for a rich collection of types beyond those of PLI, we explored the Algol68 type system as a basis for the types of this logic, and we explored various constructive set theories such as Myhill's CST. Logical assertions were added to the type system. In the course of reading Myhill, we discovered the 1973 paper of Per Martin-Löf. This created a major discontinuity in our work. We saw that Martin-Löf's type theory was more powerful and elegant than Algol68 and that he treated assertions as types which created an even smoother integration of assertions and types than ours. We developed a programming logic based around PL/CV and our version of a constructive type theory.
Another major discontinuity in our work was Joe Bates' idea that we should base a programming logic around the notion that proofs and programs were best developed by progressive refinement. He combined this idea with Constable's notion that proofs are programs and designed a programming logic called PRL for his PhD thesis.
Many of our contributions to logic are in the realm of type theory. We extended the Martin-Löf type theory of 1982 to include types important for programming. The new types are subset types and quotients introduced at the Foundations of Computation meeting in 1983 in Sweden, and the inductive types introduced at the LICS meeting in 1985 and the co-inductive types introduced at the LICS meeting in 1986. We also introduced the idea of direct computation into the rules of the logic that allowed us to reduce a term in place and type uses of the Y combinator.
It was not until Howe's seminal results on computational equality at the LICS 89 meeting that we knew that these reductions were valid in all contexts. Howe's proof that computational equality is a congruence over types has become a basic technique in programming language semantics. The proof technique is sometimes known as "Howe's trick."
We also extended type theory to include partial functions and partial objects. Karl Crary has extended this work recently and implemented part of the theory in Nuprl.
Lately the theory has been extended with very-dependent function types and with intersection types .
We departed from Martin-Löf's 1982 theory in a basic way by reinterpreting the meaning of a sequent in type theory. In Martin-Löf's theories, a sequent is not well-formed unless all the type expressions in the hypothesis list are known to denote types. In Nuprl, we assume that type expressions in the hypothesis list are well-formed. If the assumption is false, then the sequent is trivially valid.
Nuprl also reduced the number of basic judgements of the theory from four in Martin-Löf to one in Nuprl and introduced the notion of subtypes.
One of the most significant logical contributions of our work is Stuart Allen's nontype theoretic semantics based on per's (partial equivalence relations). This semantics is given in Allen's PhD thesis. We have used this semantics to prove the consistency of many extensions to Nuprl.
We also extended the propositions-as-types notion to classical logic in a paper called Semantics of Evidence part of which appears as
Chetan Murthy made a fundamental contribution to classical semantics by showing how to use control operators to realize classical propositions such as excluded middle.
Another major contribution to semantics is the recent work of Doug Howe on reconciling subsets of Nuprl with classical semantics.
We have been concerned with a formal metatheory and reflection since the beginning of the project. One of our goals is to understand reflection better. Another has been to use reflection to justify the correctness of extensions of the type theory via decision procedures. We have also used reflection to account for the computational complexity of extracted programs and for defining resource bounded sublogics.
The Nuprl account of a typed predicate calculus is a very interesting logic. We can control the richness of the type theory by including more of the full Nuprl theory. At the most basic level is a logic that is like the "polymorphic predicate calculus" that Milner devised for LCF. But we can also add subtyping as a basic primitive and gradually include type constructors until the result is a full blown type theory presented from a logical point of view.