A type system for Erlang

Abstract

The actor model is a concurrent computational model[4] used by a number of programming languages such as Erlang[5], which is a concurrent language that became very prevalent in today's world. It is a scalable model used for constructing reactive systems where a system consists of several actors executing asynchronously in parallel. An actor can communicate with another actor via message passing. Concurrency is hard to reason about since a program might result in multiple interleavings, leading to a nondeterministic behaviour which in tum complicate debugging. One way how to simplify reasoning is by using a type system, which is a static analyser used to approximate the behaviour of a program[7]. This is done by using a set of rules which describe what an expression will evaluate into. In this dissertation I will discuss work towards building a type system that reasons about communicating actors by using a calculus that is based on Erlang. I will give the design of the type system by first stating the errors which the system might go into and then showing the typing rules. Finally I will show that the type system works correctly by giving a proof of soundness.