Skip to main content
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 ...
Martin Berger's 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 ...
Neel Krishnaswami's 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 ...
Peter Leupold's 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 ...
Martin Berger's 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$. $\...
varkor's user avatar
  • 246
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 ...
Martin Berger's user avatar
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 ...
Martin Berger's user avatar
3 votes
Accepted

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 ...
Damiano Mazza's 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 ...
Zachary Vance's 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): ...
Martin Berger's 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 ...
Martin Berger's 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 ...
Ulrik Rasmussen's user avatar

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