# How exactly does on describe the formal semantics of the Applied $\pi$-Calculus?

In "Mobile Values, New Names, and Secure Communication", Abadí and Fournet describe thet Applied-$\pi$-Calculus. Although I understood a great part of the description of the Applied $\pi$-Calculus, I'm still a bit confused as to what exactly its formal semantics consists of.

The authors define (on page 2):

A signature $\Sigma$ consists of a finite set of function symbols, such as f, encrypt, and pairm each with an arity.

On page 3, they say that

Given a signature $\Sigma$, we equip it with an equational theory, that is, with an equivalence relation on terms that is closed under substitution of terms for variables.

Then they proceed, still on page 3, to define Structural equivalence, which also is an equivalence relation, but defined on extended processes and not terms.

So after reading the paper a number of times and consulting some other resources on the Internet, I have concluded that the semantics of the $\pi$-Calculus depends on a given signature (and hence is "parametrized" in a sense); and that it is composed of:

• the signature and its equational theory, which is provided by us, depending on the application context (I may include symmetric cryptography functions and some equations modeling their behavior, and no asymmetric constructions at all, for example);
• the structural equivalence relation for processes;
• the internal reduction relation (structural semantics used for plain processes);
• the reduction relation including interaction with the environment.

Is this correct, or did I miss anything?

You are roughly correct. From an operational point-of-view, applied-$\pi$ is 'just' a $\pi$-calculus where interesting values (rather than just pure names) can be communicated.
• Could you expand on the error of that theorem? The actual result is what? $\approx \subseteq \approx_{\ell}$ or the opposite $\approx_{\ell} \subseteq \approx$ or are the two equivalences completely unrelated? – Bakuriu Sep 17 '16 at 13:34
• They still have Theorem 4.1: Observational equivalence is labelled bisimilarity $\approx = \approx_{\ell}$. In section 4.5 they say that the claim is missing the hypothesis that exported variables must not be of channel type, otherwise there are processes that are in $\approx_{\ell}$ while not being $\approx$, they mention a paper by Liu where adding this hypothesis he is able to prove the theorem and argue that for their variant of the calculus and semantic the hypothesis is not needed, so it looks like they still think that the theorem is true. – Bakuriu Sep 18 '16 at 11:16