The Erlang compiler compiles Erlang code to Core Erlang. Core Erlang is a simplified intermediate representation of Erlang: still human-readable, but more regular and with a simpler semantics than Erlang source code. Core Erlang was developed in collaboration between the Department of IT at Uppsala University and Ericsson's OTP/Erlang developers.
The goal of this project is to formally define the semantics of (a subset of) Core Erlang in the interactive proof assistant Isabelle. Isabelle is a software tool that allows pogramming languages and their semantics to be defined in a formal logic. This logic offers both concepts from programming (e.g., datatypes, recursive functions) and mathematical concepts (e.g., quantifiers).
This project will allow you to become familiar with Isabelle, one of the world's leading software tools to assist with the development of formal proofs.