9

My answer is really just an elaboration of Gilles', that I had not read before I wrote mine. Maybe it's nevertheless helpful. Let me begin my attempt at answering your question with a distinction between two dimensions of programming languages work that relate quite differently to programming language theory in general and process calculus in particular. ...


8

The science of programming language design is very much in its infancy. Theory (the study of what programs mean and of the expressivity of a language) and empiricism (what programmers manage or don't manage to do) give a lot of qualitative arguments to weigh one way or another when designing a language. But we rarely have any quantitative reason to decide. ...


8

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 ambient $\pi$-calculus is and exactly what feature you are encoding. For sums you need to realise that there are different kinds of sums for example input ...


5

There are not that many books on this subject, as it continues to evolve at a rapid pace. Classic books on process calculi (that don't focus on π-calculus-like mobility) are: C. A. R. Hoare, Communicating Sequential Processes. A. W. Roscoe, The Theory and Practice of Concurrency. M. C. B. Hennessy, Algebraic Theory of Processes. R. Milner, Concurrency ...


5

Legally speaking, the term "calculus" is almost always used to describe a language, i.e., a piece of syntax, with added rules of calculation or reasoning. Examples include the good old predicate calculus, lambda calculus, process calculi, various type theories and logics (e.g., Martin-Lof type theory and linear logic). From a programming language point of ...


3

Q1: Yes, every LTS is bisimilar to its unfolding, which is a tree. Q2: No, by a cardinality argument. For instance take infinite binary trees with $L=\{a,b\}$. Each tree has countable set of states and is finitely-branching, but you have uncountably many such trees, even up to bisimilarity. However you have only countably many $\mu$-calculus formulas, so ...


3

I see so many variants on the Pi-calculus out there and there is a lot of active research, but will they ever be needed or have important applications? The reason why I ask is because I love developing programming languages and the true end goal would be to use the theory to actually build a PL. For the stuff I have written, there really has not been any ...


1

You say that "the true end goal would be to use the theory to actually build a PL." So, you presumably admit that there are other goals? From my point of view, the No. 1 purpose of theory is to provide understanding, which can be in reasoning about existing programming languages as well as the programs written in them. In my spare time, I maintain a large ...


1

There is a paper by Van Beek called An Algebraic Approach to Transactional Processes which describes adding transactions to process algebra: (a :~ 0 . a:~ a + 2) II (a:~ 1 a:~ a X 2) ((a :~ 0 . a:~ a + 2)) II ((a:~ 1 a:~ a X 2)) This paper even delves into isolation levels. The author describes how in Communicating Sequential Processes (CSP), if you have ...


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