A Sorted Semantic Framework for Applied Process Calculi

(Link).

Authors: Johannes Borgström, Ramūnas Gutkovas, Joachim Parrow, Björn Victor and Johannes Åman Pohjola (Uppsala University)

Reference: Retrieved from Joachim Parrow's homepage, 16 April 2013.

Comments: After some time away from the blog due first to conference travel, then to the next round of conference submission, a number of papers have collected in my Google Scholar Updates in-tray. This week sees an unpublished paper that, judging from its length of exactly 15 pages (not counting appendices) must also be a conference submission - wrestling scientific work to exactly fit the page length requirements of this or that venue is one of the necessary frustrations of being a researcher.

A very common mode of research in theoretical computer science is to study formal calculi, which are often best seen as idealised programming languages, usually with a very simple syntax and set of operations. These calculi allow various aspects of computation to be formalised and studied without all the impurities and hacks that go along with a 'real' programming language intended to be conveniently usable. The most famous and important such calculus is the λ (lambda) calculus, which I discussed a few posts back.

Almost as important are the calculi known collectively as the process calculi, which are intended for the formalisation and study of concurrent computation - computation that runs in parallel (perhaps simultaneously) in different threads, occasionally interacting. This is an important topic because computers - even home PCs - are increasingly multiplying the number of separate 'cores' in their hardware, not to mention the use of massively distributed computation across the internet; yet what the best programming languages, methodologies, and theory should be for this sort of architecture remains very much up for grabs.

The process calculi best known to me is the π (pi) calculus, introduced by Robin Milner, Joachim Parrow (one of the authors of this paper), and David Walker here. This notion of process calculus alone has produced dozens of offshoots and modifications, often aimed at some specific application. To name just one important example, the spi calculus is used to formalise cryptographic protocols.

At one level this paper merely adds to the arguably overstocked zoo of process calculi, by making modifications to the existing psi-calculus by adding a sort system (a concept I discussed, in a rather different setting, here) and more flexible pattern matching. At another level, this paper is intended to be a unifying and clarifying contribution to the zoo, by setting the augmented psi-calculus up as a system that captures many other process calculi. By this the authors don't mean that the new and improved psi-calculus makes systems like the spi calculus practically redundant; rather, the spi calculus can be seen in a some relatively natural way as a particular instantiation of the psi-calculus. The advantage of this, as posited in the introduction, is that basic theoretical proofs about process calculi only need to be 'done once', for the very general psi-calculus, and then can be exported 'for free' to hold for the many process calculi that are examples of the psi-calculus. With these basic correctness proofs out the way, people can then direct their attention to what really is unique, interesting or useful about the calculus they are particularly interested in.