TL;DR
This paper presents a formal, proof-assistant-based model of a subset of Erlang to verify the correctness of program refactorings through rigorous proofs.
Contribution
It introduces a formal semantics of Erlang in a proof assistant, enabling machine-checked proofs of language properties and refactoring correctness.
Findings
Formal syntax and semantics of a subset of Erlang
Proofs of properties like determinism
Verification of simple refactoring strategies
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
