What's the difference between Moggi's computational metalanguage and Moggi's lambda calculus? This is a reference confusion. Sometimes I see people use the term "Moggi's computational metalanguage" to refer to the calculus presented by Moggi, and sometimes to "Moggi's computational lambda calculus". Sometimes they use $\lambda_{ml}$ and sometimes $\lambda_c$.

I've always assumed they are both the same thing, but reading the abstract from a talk by Katsumata and Moegelberg, it says:


  we show the fullness of Moggi's monadic translation from the computational lambda calculus $\lc$ with sums to the computational metalanguage $\lml$ with sums using TT-lifting and TT-closure operator.


Aren't these languages the same thing? Where are they introduced specifically with these names? It seems like Moggi sometimes talks about $\lambda_c$ model for what he calls a metalanguage, but then in other paper he talks about computational lambda calculus.
The terminology can be a bit confusing but yes there are two languages
in for instance Moggi's "Notions of Computations as Monads" (free link
here: https://core.ac.uk/download/pdf/21173011.pdf).

In that paper, the languages are called $\lambda_{ml}$, the
metalanguage, and $\lambda_{pl}$ the "programming language". I believe
$\lambda_{pl}$ plays the role of the computational lambda calculus but
I may be mistaken.
One confusing aspect is that both languages have an explicit type
constructor $T$ representing the monad, but they are used differently.

$\lambda_{ml}$ is a "pure" language with a monad $T$, i.e., all
manipulation of the monad is explicit in the types and the function
type $\tau_1 \to \tau_2$ is the type of pure functions. Observe the
bind rule (from figure 3 on page 9):

$$\frac{x   : \tau \vdash_{ml} e_1 : T \tau_1 \quad
        x_1 : \tau_1 \vdash_{ml} e_2 : T \tau_2 }
       {x :\tau \vdash_{ml} let_T x_1 \Leftarrow e_1 in e_2 : T \tau_2}$$

$e_1$ and $e_2$ are explicitly typed as terms of $T \tau_1, T\tau_2$
to mark that they are effectful. Every effectful expression is really
a pure term with monadic type. This is similar to how we program with
monads in Haskell where Haskell plays the role of the metalanguage and
the monad encodes effects but really we are always manipulating "pure"
terms (I put "pure" in quotes as Haskell has its own effects of
divergence and error).

We can see this in the semantics of the metalanguage: a term $x:\tau
\vdash_{ml} e : \tau'$ denotes a morphism $[\tau] \to [\tau']$, the
monad doesn't arise unless we mention it.

On the other hand, $\lambda_{pl}$ is intended to be an effectful
call-by-value programming language. As such a term $x : \tau
\vdash_{pl} e : \tau'$ is a possibly effectful term that returns
values of type $\tau'$, similar to languages like SML and OCaml. That
is why in the paper the function type is written $\tau \rightharpoonup
\tau'$ because it is the type of effectful functions, not pure
functions.

Compare the bind rule here (from figure 5 on page 11):
$$\frac{x   : \tau \vdash_{pl} e_1 : \tau_1 \quad
        x_1 : \tau_1 \vdash_{pl} e_2 : \tau_2 }
       {x :\tau \vdash_{pl} let x_1 \Leftarrow e_1 in e_2 : \tau_2}$$

The monad doesn't appear explicitly, but in the semantics this uses the
Kleisli extension of $e_2$.
In the semantics, we see that the terms of the programming language
are interpreted in the Kleisli category of the monad, so a term $x :
\tau \vdash_{pl} e : \tau'$ denotes a morphism $[\tau] \to T[\tau']$.

$\lambda_{pl}$ does include an explicit monad constructor $T$, which
SML and OCaml don't have as a primitive type constructor because $T a$
is equivalent to unit -&gt; a because -&gt; means effectful function.