Turán, Gergő Lajos, Fomin, Arsenii, Bereczky, Péter, Horpácsi, Dániel, Thompson, Simon (2025) Deriving an Erlang interpreter from a mechanised formal semantics of Core Erlang. In: Erlang '25: Proceedings of the 24th ACM SIGPLAN International Workshop on Erlang. . pp. 26-39. Association for Computing Machinery E-ISBN 979-8-4007-2144-1. (doi:10.1145/3759161.3763046) (KAR id:111662)
|
PDF
Publisher pdf
Language: English 
This work is licensed under a Creative Commons Attribution 4.0 International License.
|
|
|
Download this file (PDF/1MB) |
Preview |
| Request a format suitable for use with assistive technology e.g. a screenreader | |
| Official URL: https://doi.org/10.1145/3759161.3763046 |
|
Abstract
We present an interpreter for Erlang in Haskell, derived from a formal semantics for Core Erlang mechanised in Coq. The interpreter function is derived from the Coq inductive definitions that make up the semantics by extracting Haskell code from Gallina functions provably equivalent to the inductive definitions, and optimising the result. The semantics is inherently non-deterministic, and it is made deterministic by introducing a scheduler component; we also present a computation graph that shows all the non-deterministic choices that arise during computation. The paper concludes with an evaluation of the work and preliminary performance data.
| Item Type: | Conference or workshop item (Paper) |
|---|---|
| DOI/Identification number: | 10.1145/3759161.3763046 |
| Uncontrolled keywords: | Erlang; core Erlang; formal semantics; formally based interpreter; Scheduling, Coq; Rocq; Haskell |
| Subjects: | Q Science > QA Mathematics (inc Computing science) |
| Institutional Unit: | Schools > School of Computing |
| Former Institutional Unit: |
There are no former institutional units.
|
| SWORD Depositor: | JISC Publications Router |
| Depositing User: | JISC Publications Router |
| Date Deposited: | 02 Feb 2026 09:46 UTC |
| Last Modified: | 04 Feb 2026 03:45 UTC |
| Resource URI: | https://kar.kent.ac.uk/id/eprint/111662 (The current URI for this page, for reference purposes) |
University of Kent Author Information
Thompson, Simon.
| Creator's ORCID: |
 https://orcid.org/0000-0002-2350-301X
|
|---|---|
| CReDIT Contributor Roles: |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):
Altmetric
Altmetric
