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$. $\alpha$-equivalence and capture-avoiding substitution is an important concept to understand in type theory: I would recommend studying this concept for the ...


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 you're looking for, but it might be interesting to learn about. For an example, the ambient calculus. The process calculus wikipedia page includes some others.


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 for synchrony and asynchrony. 1983. https://www.sciencedirect.com/science/article/pii/0304397583901147

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