Presenter
Péter Bereczky
Eötvös Loránd University, Faculty of Informatics
Authors
Péter Bereczky
Abstract
Refactoring tools are essential for software maintenance, yet they are rarely formally verified-causing developers to rely on manual transformations due to a lack of trust. This issue served as the motivation for our research over recent years: a machine-checked formalisation of Core Erlang, the sublanguage of Erlang, which is an impure functional programming language featuring strict evaluation, uncurried function abstractions, lightweight processes, and asynchronous communication. By using a formal semantics of Core Erlang and suitable program equivalence definitions, we can prove that a refactoring is correct if the programs before and after transformation are equivalent (i.e. they behave the same way).
This talk presents key results from our work: a reduction-style formal semantics for both the sequential features and a representative concurrent subset of Core Erlang, along with multiple semantics-based program equivalence concepts. We discuss how these equivalence definitions-including barbed bisimulation for concurrent setups-were successfully applied to verify the correctness of program refactorings and optimisations. Finally, we highlight our experiences and insights from machine-checking these formal definitions, equivalences, and proofs in the Rocq proof assistant. Beyond proving behaviour preservation, this formal framework also serves as the foundation for our current research: building a formally verified Erlang compiler.
Slides
TBA