Skip to main content

Machine-checked natural semantics for Core Erlang: exceptions and side effects

Bereczky, Péter and Horpácsi, Dániel and Thompson, Simon (2020) Machine-checked natural semantics for Core Erlang: exceptions and side effects. In: Proceedings of the 19th ACM SIGPLAN International Workshop on Erlang. ACM, pp. 1-13. ISBN 978-1-4503-8049-2. (doi:10.1145/3406085.3409008) (KAR id:82515)

PDF Author's Accepted Manuscript
Language: English


Creative Commons Licence
This work is licensed under a Creative Commons Attribution-NoDerivatives 4.0 International License.
Download (715kB) Preview
[img]
Preview
Official URL
https://doi.org/10.1145/3406085.3409008

Abstract

This 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 an extended natural semantics for Core Erlang based on our previous formalisation implemented with the Coq Proof Assistant. This extension includes the concepts of exceptions and side effects, moreover, some modifications and updates are also discussed. Then we describe theorems about the properties of this formalisation (e.g. determinism), formal expression evaluation and equivalence examples. These equivalences can be interpreted as simple local refactorings.

Item Type: Book section
DOI/Identification number: 10.1145/3406085.3409008
Uncontrolled keywords: formal semantics, natural semantics, Erlang, Coq, exceptions, side effects
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: Faculties > Sciences > School of Computing
Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Simon Thompson
Date Deposited: 19 Aug 2020 09:07 UTC
Last Modified: 20 Aug 2020 10:03 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/82515 (The current URI for this page, for reference purposes)
Thompson, Simon: https://orcid.org/0000-0002-2350-301X
  • Depositors only (login required):