Looking at the striking parallels between combinatory logic and concatenative languages makes me wonder how many theorems of the former hold in the latter. The Church-Rosser theorem is particularly interesting because it would justify the use of transparent quotations. Is there any concatenative programming language proven to be Church-Rosser?
SK combinators are Church-Rosser.
However, the usual $\lambda$-calculus method of proving local confluence and then appealing to Newman's lemma doesn't work. You need a slightly fancier argument, and the SEP entry on combinatory logic gives a sketch of a proof that does work.