Dániel Horpácsi

Assistant Professor at ELTE Budapest

Dániel Horpácsi did his PhD in static analysis and program transformations, he has a particular interest in trustworthy refactoring in functional languages. He is currently leading a research group that works on machine-checked formal verification of refactoring in Erlang.

Program Equivalence in Sequential Core Erlang

AUTHORS: Péter Bereczky and Dániel Horpácsi  

Our research aims to reason about the correctness of scheme-based refactoring transformations of Erlang programs. Recently, we have developed formal semantics for sequential Core Erlang in Coq in order to use it as a stepping stone towards our goal and investigate program transformations in Core Erlang. Refactoring, by definition, means transforming programs to semantically equivalent programs; thus, the correctness of the transformations depends on both the definition of semantics and how we characterize equivalence.  

In this extended abstract, we overview some possible formalisations of expression equivalence for Core Erlang, focusing on different kinds of simple behavioural equivalences which we have already formalised in Coq. We also show some use cases, and outline our short term future plans which include investigating other possible approaches to define program equivalence (for example contextual equivalence, and reasoning about behavioural equivalence using a dedicated logic).

Slides
←Back