How can I prove formally semantic equivalence of programming languages?
Comparing two programming languages is difficult  is a difficult
problem, and far from being solved. The key issue is that there are many different ways languages can be compared, and none of them is compelling. 

The most widely used approach, coming from logic, is to 
consider translations between the languages to be compared.
The general
idea is as follows:  if we 
have a translation into from $L_1$ into $L_2$, say, then 
$L_2$ is at least as expressive as $L_1$.

Unfortunately, things are not quite that easy. 
By the Church-Turing thesis you know that you can 
always find such translations
(for Turing-complete languages). So the very existence of
translations is not discreminating enough to distinguish
programming languages. And yet, everybody who has programmed in
different languages (e.g. Assembler vs Scala) knows that some
languages are easier to program than others. 

This conundrum is
usually approached by putting restrictions on what counts as a
translation functions. The idea here is  that the translation functions
'measure' how much 'rearrangement' is necessary when translating
from one language to the other: the more 'rearrangement'
required, the less expressive the target language. Restrictions
on translations control what kind of 'rearrangement' we consider.
If we can show that
no translation exists that satisfies a bunch of restrictions, then
the languages are substantially different in expressivity.

In this sense e.g. the $\pi$-calculus is very expressive because
we can often find translations meeting various restrictions when
translating from a language $L$ into the $\pi$-calculus. Conversely, 
purely functional languages are not so expressive, because when we
translate $L$ into a purely functional language, the translation functions
often violate various constraints.

Here is a far from exhausting list of popular restrictions
for this purpose:


The translation should preserve termination.
The translation should preserve the structure of
programs (mathematically: translation should be a
homomorphism): $$trans(f(P_1, ..., P_n)) = trans(f)(trans(P_1),
  ..., trans(P_n)).$$ This constraint is usually referred to as
compositionality of the translation.
While compositionality can often not be achieved when we try to
compare very different languages $L_1$ and $L_2$, A weaker form
almost always holds: (simplifying a bit) there is a fixed
program $Q$ for each constructor $f$ such that $$trans(f(P_1, ..., P_n)) = trans(f)(Q,
  trans(P_1), ..., trans(P_n)).$$ I like to call this
compositionality-up-to-OS, because the fixed program $Q$ acts
like an operating system.
The translation should preserve the (asymptotic space or time)
complexity of programs. (The Slot and van Emde Boas thesis says
that polynomial-time translations are always possible, so we
might need finer distinctions than preservation of run-time up
to a polynomial factor.) The theory of NP-completeness can be
seen in this light.
The translation should exhibit operational correspondence: We
say an encoding $trans(.)$ is operationally corresponding if it is
Whenever $P →^* Q$ then $trans(P) →^*≈ trans(Q)$. Moreover, whenever $trans(P) →^* Q$ then there is $P'$ such that $P
  →^* P'$ and $Q →^*≈ trans(P')$. Here ≈ is the chosen notion of program 
equality in the target language.
Divergence reflection: this means that whenever $trans(P)$ diverges, then so does $P$.
Success sensitiveness: Given a criterion of program
success (e.g. the ability of output a chosen value) on both
source and target, an encoding $trans(.)$ is success sensitive if $P$
is successful if and only iff $trans(P)$ is successful.
Full abstraction, we want $P \simeq_1 Q$ iff $trans(P) \simeq_2 trans(Q)$,
where $\simeq_1$ is the chosen notion of program equality in the source language
of the translation and $\simeq_2$ does that job in the target.
Preservation of program size:  the translation should not lead to substantial
increases in program size.
Name invariance: each program has a finite number of
'interaction points' that the outside can use to interact with
the program, e.g. free variables.  We can require that
encodings commut with injective renamings of 'interaction
points'.


The relationships between those criteria, like the whole field
of programming language expressiveness, is ill-understood.

A pioneering paper in the study of programming language expressiveness is


M. Felleisen, On the Expressive Power of Programming Languages.


where key concepts from logic, such as conservative extension of
theories are generalised to programming languages.