Abstract:
In this talk, I will introduce the small-step operational semantics we developed for the Core Erlang language and implemented in the Rocq proof assistant. I will discuss the various design decisions we explored and adopted, including variable and binding representations, substitutions versus environments, and the validation of the mechanised semantics. I will also explain how we defined notions of program equivalence that coincide with behavioural equivalence. Then, I will highlight several applications of the semantics that contribute to trustworthy software tools for Erlang, including the verification of refactoring correctness, the formalization of software vulnerabilities, and a verifier for property-based tests. Finally, I will present the early but promising results of our most recent effort: the development of a proven-correct optimizing compiler for Erlang.
Short Bio:
Dániel Horpácsi is an assistant professor at Eötvös Loránd University. His research focuses on using formal methods for developing trustworthy tools for program analysis and transformation. He co-developed a mechanised formal semantics for Core Erlang to support verification of Erlang programs and their transformations. He is currently the principal investigator of a project aimed at developing a provably correct optimizing compiler for Erlang.
