A Proof Assistant Based Formalisation of Core Erlang
Abstract
Our research is part of a wider project that aims to investigate and reason about the correctness of scheme-based source code transformations of Erlang programs. In order to formally reason about the definition of a programming language and the software built using it, we need a mathematically rigorous description of that language. In this paper, we present our proof-assistant-based formalisation of a subset of Erlang, intended to serve as a base for proving refactorings correct. After discussing how we reused concepts from related work, we show the syntax and semantics of our formal description, including the abstractions involved (e.g. closures). We also present essential properties of the formalisation (e.g. determinism) along with their machine-checked proofs. Finally, we prove the correctness of some simple refactoring strategies.
Cite
@article{arxiv.2005.11821,
title = {A Proof Assistant Based Formalisation of Core Erlang},
author = {Péter Bereczky and Dániel Horpácsi and Simon Thompson},
journal= {arXiv preprint arXiv:2005.11821},
year = {2020}
}
Comments
21st International Symposium on Trends in Functional Programming