The so-called Curry-Howard isomorphism has emerged as the foundation of the relationship between constructive logic and computation. Under this analogy, propositions correspond to types, proofs correspond to terms in typed &lgr;-calculus, and normalization of proofs induces reduction of terms to normal form. Furthermore, from a normalized proof of a formula ∃ z . A ( x , z ), one can extract a particular term t and a proof of A ( x , t ), provided that the assumptions of the original proof are of a certain class called Harrop formulas. This observation is the theoretical foundation of logic programming.

This paper considers a variant of Gentzen’s presentation of proof theory, using instead the Borkowski-Slupecki rule for the elimination of the existential quantifier. The two formalisms determine the same set of provable formulas, but they behave differently with respect to proof normalization. Indeed, the crucial observation of this paper us that, for proofs in the Borkowski-Slupecki system of existential formulas as above, one can extract a partial answer before the proof is totally normalized. The author defines the notion of pseudonormal proof for the new system, which formalizes these partial answers.

The most striking consequence of this approach is that (pseudo)normalization can now treat proofs involving infinite objects. This approach provides a logical foundation, in the sense of the Curry-Howard isomorphism, for computation with infinite data objects (that is, lazy computation, over data domains with nonstrict constructors.

This paper is a valuable contribution to an important line of research, the application of proof theory to the theory of computation. It is not the place to begin reading about proof normalization--familiarity with the basic literature in proof theory is assumed--but it is carefully written and generous in providing examples.