Normalization, cut-elimination, and the theory of proofs - Ungar, A. M. (Anthony M.), 1945- (CSLI, 1992)