You are right. In Romania we also prove that different computational models are equivalent (Turing machine, lambda calculus, Markov machine, logic programming)

>prove that different computational models are equivalent (Turing machine, lambda calculus, Markov machine, logic programming)

Is there a text which guides how to write such a proof?

i remember covering this sort of thing in my automata theory class. we used this textbook: https://www.amazon.com/Automata-Computability-Complexity-The...

I can't remember if it specifically shows such a proof in there, but you might look at courseware for automata theory and such.

In general, from what I remember, you would use a general technique called "reduction", where you try to make two problems equivalent, "reducing" solving one to the problem of solving the other one, kind of mapping one problem on to another, so that solving one solves them both. So, you reduce running an arbitrary Turing machine, to say, lambda calculus, almost like you write a "compiler" from a Turing machine with lambda calculus as the target language. Then, you reduce computing in lambda calculus to a Turing machine. So, then you know that each can compute what the other computes, and they can only compute the same things. If you only did one half, one reduction, you would only know, say, that a Turing machine could do everything you could do in lambda calculus, but it would leave the possibility that the Turing machine could compute things lambda calculus can't.

Generally, implement/simulate one in the other.