Skip to main content
Kent Academic Repository

A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang

Bereczky, Péter and Thompson, Simon and Horpacsi, Daniel (2020) A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang. In: Byrski, Aleksander and Hughes, John, eds. Trends in Functional Programming: 21st International Symposium, TFP 2020, Krakow, Poland, February 13–14, 2020, Revised Selected Papers. Lecture Notes in Computer Science, 12222 . Springer, Cham, pp. 139-158. ISBN 978-3-030-57761-2. (doi:10.1007/978-3-030-57761-2_7) (KAR id:82503)

Abstract

We present a 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. the concept of a closure). We also present essential properties of the formalisation (e.g. determinism) along with the summary of their machine-checked proofs. Finally, we prove expression pattern equivalences which can be interpreted as simple local refactorings.

Item Type: Book section
DOI/Identification number: 10.1007/978-3-030-57761-2_7
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, > QA76.76 Computer software
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: S. Thompson
Date Deposited: 18 Aug 2020 13:59 UTC
Last Modified: 16 Feb 2021 14:14 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/82503 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.