Towards an Isabelle/HOL formalisation of core Erlang
Joseph R. Harrison · 2017
As part of broader work to improve the safety of Erlang systems, we are attempting to detect (and prevent) messages which remain forever unreceived in process' mailboxes using a mix of static and runtime analysis. We have formalised the communicating portion of Core Erlang using Isabelle/HOL, an interactive theorem prover. We can use the Isabelle toolchain to prove properties of our model, automatically prepare documents, and generate verified executable code in a variety of functional programming languages.