ICFP/SPLASH 2025 (series) / Erlang 2025 (series) / Erlang 2025 /
Deriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang
This program is tentative and subject to change.
Sun 12 Oct 2025 11:38 - 12:15 at Seminar Room 7 - Formal Semantics & Verification Chair(s): Daniel Gorin
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 function; 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, including preliminary performance data.
This program is tentative and subject to change.
Sun 12 OctDisplayed time zone: Perth change
Sun 12 Oct
Displayed time zone: Perth change
11:00 - 12:30 | |||
11:00 38mTalk | Mechanised Proofs of Atom Exhaustion in Erlang Erlang Arsenii Fomin Eötvös Loránd University, Péter Bereczky Eötvös Loránd University, Dániel Horpácsi Eötvös Loránd University, Gergő Lajos Turán Eötvös Loránd University | ||
11:38 37mTalk | Deriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang Erlang Gergő Lajos Turán Eötvös Loránd University, Arsenii Fomin Eötvös Loránd University, Péter Bereczky Eötvös Loránd University, Dániel Horpácsi Eötvös Loránd University, Simon Thompson University of Kent (UK) | ||
12:15 15mTalk | (Lightning Talk) The State of The Unions: challenges for type-checking unions and generics at WhatsApp Erlang Maxwell Heiber Meta |