As part of broader work to detect orphan messages in Erlang systems using a mix of static and runtime analysis, we have formalised the communicating portion of Core Erlang using Isabelle/HOL, an interactive theorem prover. Isabelle allows us to prove properties of our system, prepare LATEX output, and generate verified executable code in a variety of functional programming languages.

We formally model a communicating fragment of Core Erlang in a language we call CoErl. The process-local and concurrent semantics of the language are modelled using a labelled transition system. We also introduce the notion of traces which capture communication events during process execution. This is followed by some illustrative examples of the concurrent semantics.

Although the model is a solid foundation, it lacks support for higher-order and recursive behaviour. Isabelle proved practical for the formalisation and verifying several properties of CoErl and its trace system, although ongoing and future work focuses on bringing the language to feature parity with Core Erlang and Erlang/OTP to provide a suitable formal model for reasoning about real Erlang programs.

PhD Candidate in the School of Computing.