10 votes

Is scope extrusion necessary in the Pi-calculus?

Scope extrusion is the key advance of $\pi$-calculus over earlier calculi such as CCS. Scope extrusion is the source of $\pi$-calculus' power of expressing (in a succint and compositional way) other ...
user avatar
10 votes

Is scope extrusion necessary in the Pi-calculus?

If we separate the notion of channel names from variables, we can make the ν-binder a true binder where the variable following ν is a normal bound variable and we only need to add a reduction rule for ...
user avatar
8 votes
Accepted

Can choice or sequential execution be expressed with other basic operators of the pi calculus?

This is a really interesting question and only partially understood. The $ \newcommand{\OUT}[2]{\overline{#1} #2 } $ precise answer to such questions depends in subtle ways on exactly what the ...
user avatar
7 votes

Are there protein-based computational models?

Membrane Computing is a model that is based on the possibility or not of movement of molecules through membranes; also on possible reactions of these molecules inside a membrane compartment. While ...
user avatar
7 votes
Accepted

Determinism and pi-calculus

There are plenty such typing systems. Most work is based on the linear/affine typing system introduced in (1) and generalised in (2). Here are the main works on this subject. In (3) the typing system ...
user avatar
4 votes
Accepted

Pi-calculus (or session types) - proof for weakening lemma

You should $\alpha$-rename to avoid conflict with the variable names. That is, you should prove weakening of the form: $\Gamma \vdash (\upsilon y) P$ implies $\Gamma, x : T \vdash (\upsilon y) P$. $\...
user avatar
  • 196
3 votes

How exactly does a compatible reduction relation change the $\pi$-calculus?

Interesting question. As Damiano says, while syntactically trivial a change, the π-calculus with non-blocking inputs is a different model of computing. (A very different one, and an extremely ...
user avatar
3 votes

How exactly does a compatible reduction relation change the $\pi$-calculus?

I don't know "exactly" how it changes the calculus, in the sense that I don't have a formal statement measuring the difference (and I am not aware that there exists one), but allowing ...
user avatar
3 votes

Encoding an infinitely looping process with state in the pi-calculus

The process $P{\langle 0, c, d\rangle}$ in the context of a recursively defined process like $$ P{\langle count, c, d\rangle} \quad\stackrel{\text{def}}{=}\quad c(v).(\overline{d}\langle count+v ...
user avatar
3 votes

Scope of active substitutions in the applied $\pi$-calculus

The key to understanding scope management in $\pi$-calculi is to look at the structural congruence $P \equiv Q$ and at the notions of free name $\newcommand{\FN}[1]{\text{fn}(#1)}\FN{P}$ and free ...
user avatar
2 votes

Sequential execution in π-Calculus

Sequential execution is an edge case of concurrent computation. Robin Milner said this clearly in his Turing award lecture "Elements of interaction" (CACM, 36(1), 1993): ...
user avatar
2 votes
Accepted

Semantic equivalence using a model of computation of two languages

Let me clarify the setting, which has nothing to do with $\pi$-calculus or bisimulation. The first thing you have to realise that it does not make much sense to talk about a programming language ...
user avatar
2 votes

Are there protein-based computational models?

There are models of how to compute with arbitrary chemical reactions using molecules that drift around and randomly collide. They crop up in parallel computing models sometimes. It's probably not what ...
user avatar
1 vote

Reference request: pi-calculus with simultaneous events

Milner defines the SCCS calculus in [1]. This is a generalization of CCS where the actions form an abelian group, and where the communication rule is defined as in my question. [1] Milner, R. Calculi ...
user avatar

Only top scored, non community-wiki answers of a minimum length are eligible