Content area
This project formalizes the semantics of a subset of Core Erlang, an intermediate representation used by the Erlang compiler, using the proof assistant Isabelle/HOL. The study begins by defining the abstract syntax of Core Erlang, including its lexical elements, terminals, and non-terminals. It then advances to formalizing the static semantics, focusing on module definitions, variable scopes, and the correct binding of function parameters. The dynamic semantics are modeled using big-step operational semantics to evaluate expressions and handle constructs such as recursive functions, pattern matching, exceptions, and undefined behavior.
The research emphasizes using Isabelle/HOL’s powerful reasoning capabilities to define and verify the correctness of these semantics. In doing so, it addresses the challenges posed by recursive functions and their termination, utilizing Isabelle’s tools for automatic proof generation while marking unresolved subgoals with placeholders. Additionally, the study explores the potential for extending this formalization to more complex constructs of Core Erlang. It highlights the importance of incorporating proof strategies to validate the operational semantics.
The outcomes of this project contribute to a deeper understanding of Core Erlang’s formal properties and showcase the effectiveness of Isabelle/HOL in formalizing the semantics of functional programming languages. This formalization lays a robust foundation for future work, including extending the framework to parse and evaluate actual Core Erlang code and proving the correctness of the semantics through formal theorems in Isabelle.