A Formal Semantics of Core Erlang

Erlang is a high-level functional programming language. Its run-time system is designed for distributed, fault-tolerant and highly available systems. Originally developed for telephony switches by Ericsson, the language is now in use in a wide range of industries - for instance, WhatsApp is written in Erlang.

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.

Work environment:
Isabelle (Windows/macOS/Linux)
Useful knowledge/skills:
Functional programming, first-order logic, programming language semantics
Tjark Weber

Last modified: 2023-11-05