This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Program Equivalence in Sequential Core Erlang by Péter Bereczky, Dániel Horpácsi ABSTRACT 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). --- SPEAKER - Péter Bereczky Machine-checked formal semantics for verifying refactorings! Peter is an enthusiastic PhD student at Eötvös Loránd University, Budapest. His interests include formal software verification which is why he joined the High-Assurance Refactoring Project, where the goal is to reason about the meaning-preservation of refactorings considering Erlang programs. He is currently working on formalising Core Erlang and program equivalence in Coq as a stepping stone towards formalising Erlang. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​