Lambda the Ultimate

I've read a bit about concatenative languages and how they can be modeled, but they seem to take a mostly informal tone. I'd like to change that, so I wrote the beginnings of a formalism on a tiny subset of concatenative languages. It's available here (the important parts are in monospaced font after an introduction). This is heavily based on existing work, which I reference. The main thing I'm wondering about is, how can I make this mathematically rigorous and prove that the combinators over, dip and drop form a Turing-complete language? Or, if not, how would I prove a counterexample?

Well, the question of Turing-completeness may be a bit academic. Another issue of concern relates to type systems. If a set of type rules is defined on a language, how can it be shown that those rules are consistent with the operational semantics? I think a minimal set of combinators would be an optimal base for a correct type system, but I'm not sure.