In 1930 the Intuitionist mathematician A. Heyting [Heyting 30] presented a set of rules that characterized Intuitionistic logic and differentiated it from classical logic. In addition he formulated Intuitionistic first--order number theory (based on Peano's famous axioms) as the classical theory without the law of the excluded middle. (The Intuitionistic theory is often called Heyting arithmetic.)
In 1945 the logician S. C. Kleene proposed his well-known realizability interpretation of Intuitionistic logic and number theory [Kleene 45]. He showed that any function definable in Heyting arithmetic is Turing computable. This raised the possibility that formal systems of Intuitionistic logic could be used as programming languages. A specific proposal for this was made by Constable [Constable 71] as part of a study of very high--level programming languages and by Bishop [Bishop 70] as part of his study of constructive analysis [Bishop 67]. In 1976 Constable together with his students M. J. O'Donnell, S. D. Johnson, D.B. Krafft and D.R. Zlatin developed a new kind of formal system called programming logic [Constable 77,Constable & O'Donnell 78,Constable, Johnson, & Eichenlaub 82] which interpreted programs as constructive proofs and allowed execution of these proofs. This system is called PL/CV.
The propositions--as--types principle [Curry, Feys, & Craig 58,Howard 80] offered a new way to interpret constructive logic and extract its constructive content. These ideas came to us from [Stenlund 72,Martin-Löf 73] and were applied in the PL/CV setting in version V3 [Constable & Zlatin 84,Stansifer 85]. They were further refined by Bates [Bates 79] and became the basis for the actual Nuprl system [Bates & Constable 85,Bates & Constable 83].
Much of our recent theoretical work has focused on the Nuprl system. In his Ph.D. thesis R. W. Harper [Harper 85] investigated the relative consistency of with Martin-Löf 's theories, and he established the theoretical basis for automating equality reasoning in . S. F. Allen has studied a rigorous semantic account of type theory; some of his ideas appear in chapter 8. Mendler and Constable have studied recursive types and partial functions [Constable & Mendler 85]; some of these results appear in chapter 12.