Simulating a formally specified message based concurrent language

Abstract

The π-calculus is a process calculus which models the behaviour of concurrent processes. The main feature of this calculus is message passing abilities between the processes through channels. Kobayashi et al. introduced linear channels for the π-calculus through the linear π-calculus. They proposed a type system for the linear π-calculus that makes use of a declarative definition. This definition introduces several non-deterministic characteristics when attempting to simulate it, thus making it hard to do so. The research into linear channels goes beyond this proposed type system. Studies have shown that the linear channels can be used to encode session types using standard types or by expressing linear types as a linear process. Another study, on the other hand, defined the typing rules for such session types to match intuitionistic linear logic. Linear channels lend their uses beyond session types. Since they are essentially single use channels, they are rather useful in compiler optimisation and garbage collection as a compiler can find out, through a static analysis of the program, when a linear resource has been used up. This study analysed the declarative definition of the type system, translated it to an algorithmic definition and implemented this in the form of a static typechecker using OCaml. Also using OCaml, a parser for the targeted language, which is an extension on the linear π-calculus, was implemented. Finally, an evaluator was implemented to complete an interpreter and be able to fully test the language and type system. While the interpreter implemented was discovered to have some expected but undesired behaviour, it is quite capable of automatically testing the type system through the implementation.