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.

Thu Sep 14 08:45:18 EDT 1995