{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T05:43:09Z","timestamp":1772084589560,"version":"3.50.1"},"reference-count":6,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":16186,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1969,11,17]]},"abstract":"<jats:p>One of the basic results in the theory of \u03bb-conversion is the Church-Rosser Theorem, which says that, using certain rules for conversion and reduction of \u03bb-formulae, any two interconvertible formulae can both be reduced to one formula. (I will not explain this in detail, as \u03bb-conversion is described fully in Church's [2], where the Church-Rosser Theorem is Theorem 7 XXVII; see also Chapter 4 of Curry and Feys' [3].) The first part of the present paper contains an abstract form of this theorem.<\/jats:p>","DOI":"10.1017\/s0022481200128439","type":"journal-article","created":{"date-parts":[[2014,3,13]],"date-time":"2014-03-13T12:31:25Z","timestamp":1394713885000},"page":"545-560","source":"Crossref","is-referenced-by-count":7,"title":["An Abstract form of the church-rosser theorem. I"],"prefix":"10.1017","volume":"34","author":[{"given":"R.","family":"Hindley","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200128439_ref005","first-page":"377","article-title":"Review of \u201cA new proof of the Church-Rosser theorem,\u201d","volume":"21","author":"Rosser","year":"1956","journal-title":"this Journal"},{"key":"S0022481200128439_ref001","first-page":"16","article-title":"A new proof of the Church-Rosser Theorem","volume":"55","author":"Curry","year":"1952","journal-title":"Koninklijke Nederlandse Akademie van Wetenschappen. Proceedings. Series"},{"key":"S0022481200128439_ref002","volume-title":"The calculi of Lambda-conversion","author":"Church","year":"1941"},{"key":"S0022481200128439_ref006","unstructured":"Schroer D. E. , The Church-Rosser theorem, Ph.D. thesis, University of Illinois, Urbana, Ill., 1965."},{"key":"S0022481200128439_ref003","volume-title":"Combinatory logic","author":"Curry","year":"1958"},{"key":"S0022481200128439_ref004","doi-asserted-by":"publisher","DOI":"10.2307\/1968867"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200128439","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,22]],"date-time":"2023-03-22T10:36:18Z","timestamp":1679481378000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200128439\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1969,11,17]]},"references-count":6,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1970,2]]}},"alternative-id":["S0022481200128439"],"URL":"https:\/\/doi.org\/10.1017\/s0022481200128439","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1969,11,17]]}}}