Skip to main content

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)

PDF Author's Accepted Manuscript
Language: English


Download (537kB) Preview
[thumbnail of core_erlang_paper.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL
http://dx.doi.org/10.1007/978-3-030-57761-2_7

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: Simon 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)
Thompson, Simon: https://orcid.org/0000-0002-2350-301X
  • Depositors only (login required):

Downloads

Downloads per month over past year