López-Escobar, E. G. K. Remarks on the Church-Rosser property. (English) Zbl 0715.03025 J. Symb. Log. 55, No. 1, 106-112 (1990). By analogy with important results for lambda calculus and proof theory, the author shows that a reduction algebra is computable. E.g., a classical result of Church and Rosser on the uniqueness of the normal forms of the terms of the lambda calculus becomes: If a reduction algebra satisfies the Church-Rosser Property then it is semi-computable. Indeed, the author gives another proof of the strong normalization theorem for the impredicative second-order intuitionistic propositional calculus in a natural deduction scheme. Reviewer: A.A.Mullin MSC: 03F50 Metamathematics of constructive systems 03B40 Combinatory logic and lambda calculus 03F05 Cut-elimination and normal-form theorems Keywords:lambda calculus; proof theory; reduction algebra; Church-Rosser Property; semi-computable; strong normalization theorem for the impredicative second-order intuitionistic propositional calculus; natural deduction PDFBibTeX XMLCite \textit{E. G. K. López-Escobar}, J. Symb. Log. 55, No. 1, 106--112 (1990; Zbl 0715.03025) Full Text: DOI References: [1] Metamathematical investigation of intuitionistic arithmetic and analysis 344 (1973) [2] Proceedings of the Second Scandinavian Logic Symposium pp 235– (1971) · Zbl 0219.02001 [3] Natural deduction. A proof theoretical study (1965) · Zbl 0173.00205 [4] The lambda calculus. Its syntax and semantics (1984) [5] DOI: 10.1090/S0002-9947-1936-1501858-0 · JFM 62.0037.03 [6] Indagationes Mathematica 34 pp 381– (1972) [7] Proceedings of the Second Scandinavian Logic Symposium pp 63– (1971) This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.