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


Download (715kB) Preview
[thumbnail of EW2020 final.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Simon Thompson
Date Deposited: 19 Aug 2020 09:07 UTC
Last Modified: 16 Feb 2021 14:14 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):

Downloads

Downloads per month over past year