Machine-Checked Natural Semantics for Core Erlang: Exceptions and Side Effects
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.
Sun 23 AugDisplayed time zone: Eastern Time (US & Canada) change
10:30 - 12:00
|Machine-Checked Natural Semantics for Core Erlang: Exceptions and Side Effects|
Simon Thompson University of Kent, Dániel Horpácsi Eötvös Loránd University, Péter Bereczky Eötvös Loránd UniversityDOI
|Secure Design and Verification of Erlang Systems|
Viktória Fördős Cisco SystemsDOI
|Clojerl: The Expressive Power of Clojure on the BEAM|