Erlang '26: "A Mechanised Semantics of ..."
A Mechanised Semantics of Erlang’s References
Dániel Lukács, Péter Bereczky, and Dániel Horpácsi
(Eötvös Loránd University, Hungary)
This paper formalises Erlang references as an extension to an existing formal semantics of Core Erlang mechanised in Rocq. We define reference generation based on the evaluation state, rather than relying on a registry of previously generated references. The main advantage of this approach is that it requires considerably less modifications to the existing semantics than the registry-based approach. We argue that references generated this way are sufficiently unique because freshly generated references are guaranteed to be distinct from all references available in the evaluation state at the point of generation. Finally, we present two case studies evaluating our semantics, discuss the advantages and pitfalls of our semantics, and highlight potential enhancements and alternative approaches to formalise references. We also mechanise our results in Rocq.
Article Search
Article: icfpws26erlangmain-p8-p doi:10.1145/3830434.3830944
Erlang '26: "Set-Theoretic Type Checking ..."
Set-Theoretic Type Checking of Beginner Erlang Code: A Retrospective Study
Albert Schimpf, Stefan Wehr, and Annette Bieniusa
(RPTU University of Kaiserslautern-Landau, Germany; Offenburg University of Applied Sciences, Germany)
Erlang’s tooling ecosystem traditionally prioritizes flexibility over strict static guarantees, often leaving programming mistakes undetected until runtime. This is particularly acute in educational settings, where students accustomed to statically typed languages expect compiler-like feedback. Etylizer, a static type checker based on set-theoretic types, aims to provide stronger guarantees, but has mainly been evaluated on mature, idiomatic code. We present a retrospective study of student Erlang projects collected over five years to assess Etylizer’s behavior on novice-written code. Although only 14% of student functions carry type specifications, Etylizer still finds bugs in unannotated code.
The study also revealed that Etylizer’s exhaustiveness check spuriously rejects a class of otherwise well-typed programs: if-expressions that encode exhaustiveness in complementary comparison guards instead of ending in Erlang’s idiomatic catch-all true clause—a shape that community style guides discourage, that is rare in production code, but that beginners use markedly more often. We refined Etylizer’s type system to properly handle such programs. Evaluation on student and open-source projects shows that this refinement addresses spurious exhaustiveness rejections of the shape observed in the corpus. Our findings demonstrate that educational code can reveal limitations hidden in expert-oriented codebases and provide valuable insights for improving practical static analysis tools.
Article Search
Article: icfpws26erlangmain-p9-p doi:10.1145/3830434.3830945
Erlang '26: "Green Benchmarking of BEAM ..."
Green Benchmarking of BEAM Languages
Youssef Gharbi, István Bozó, and Melinda Tóth
(Eötvös Loránd University, Hungary)
Backend services run continuously, which makes energy use an important part of software design. This paper presents measurements from our benchmark framework for web servers running on the Erlang virtual machine. We compare Erlang, Elixir, and Gleam software using several web server frameworks under static, dynamic, and WebSocket workloads. Green software research shows that sustainability must be addressed at the application layer. Our results extend this view to BEAM web stacks under controlled load. The measurements reveal clear differences between languages and frameworks, with some stacks keeping stable throughput and lower energy under stress, while others show longer runtimes or reduced success.
Article Search
Article: icfpws26erlangmain-p6-p doi:10.1145/3830434.3830942
Erlang '26: "EMoL: Erlang Messaging and ..."
EMoL: Erlang Messaging and Monitoring over LoRa
Daniel Ferenczi, Gergely Ruda, and Melinda Tóth
(Eötvös Loránd University, Hungary; evosoft Hungary, Hungary)
Devices on the IoT edge are often low-powered microcontrollers deployed to remote locations. These devices often lack communication options, such as a TCP/IP stack, needed for Erlang features like distributed messaging or monitoring. In this paper, we present EMoL, a library we developed for cross-node messaging and monitoring of nodes communicating over the LoRa (Long Range) communication technology. EMoL offers interfaces similar to Erlang’s erlang:send/2 and erlang:monitor_node/2 functions. This comparability simplifies the use of the software architecture of regular applications to build LoRa-based distributed systems. We demonstrate that EMoL helps build distributed, reliable systems for embedded devices using a fault-tolerant leader-election algorithm.
Article Search
Article: icfpws26erlangmain-p7-p doi:10.1145/3830434.3830943
Erlang '26: "Green Benchmarking of BEAM ..."
Green Benchmarking of BEAM Languages
Youssef Gharbi, István Bozó, and Melinda Tóth
(Eötvös Loránd University, Hungary)
Backend services run continuously, which makes energy use an important part of software design. This paper presents measurements from our benchmark framework for web servers running on the Erlang virtual machine. We compare Erlang, Elixir, and Gleam software using several web server frameworks under static, dynamic, and WebSocket workloads. Green software research shows that sustainability must be addressed at the application layer. Our results extend this view to BEAM web stacks under controlled load. The measurements reveal clear differences between languages and frameworks, with some stacks keeping stable throughput and lower energy under stress, while others show longer runtimes or reduced success.
Article Search
Article: icfpws26erlangmain-p6-p doi:10.1145/3830434.3830942
Erlang '26: "A Mechanised Semantics of ..."
A Mechanised Semantics of Erlang’s References
Dániel Lukács, Péter Bereczky, and Dániel Horpácsi
(Eötvös Loránd University, Hungary)
This paper formalises Erlang references as an extension to an existing formal semantics of Core Erlang mechanised in Rocq. We define reference generation based on the evaluation state, rather than relying on a registry of previously generated references. The main advantage of this approach is that it requires considerably less modifications to the existing semantics than the registry-based approach. We argue that references generated this way are sufficiently unique because freshly generated references are guaranteed to be distinct from all references available in the evaluation state at the point of generation. Finally, we present two case studies evaluating our semantics, discuss the advantages and pitfalls of our semantics, and highlight potential enhancements and alternative approaches to formalise references. We also mechanise our results in Rocq.
Article Search
Article: icfpws26erlangmain-p8-p doi:10.1145/3830434.3830944
Erlang '26: "A Mechanised Semantics of ..."
A Mechanised Semantics of Erlang’s References
Dániel Lukács, Péter Bereczky, and Dániel Horpácsi
(Eötvös Loránd University, Hungary)
This paper formalises Erlang references as an extension to an existing formal semantics of Core Erlang mechanised in Rocq. We define reference generation based on the evaluation state, rather than relying on a registry of previously generated references. The main advantage of this approach is that it requires considerably less modifications to the existing semantics than the registry-based approach. We argue that references generated this way are sufficiently unique because freshly generated references are guaranteed to be distinct from all references available in the evaluation state at the point of generation. Finally, we present two case studies evaluating our semantics, discuss the advantages and pitfalls of our semantics, and highlight potential enhancements and alternative approaches to formalise references. We also mechanise our results in Rocq.
Article Search
Article: icfpws26erlangmain-p8-p doi:10.1145/3830434.3830944
Erlang '26: "Towards Exact Semantic Equivalence ..."
Towards Exact Semantic Equivalence of Erlang BEAM Constructs: Lessons from Advanced Emulation and Decompilation
Gregory Morse and Melinda Tóth
(Eötvös Loránd University, Hungary)
Erlang offers three practically relevant ways to run code: evaluating abstract syntax trees with erl_eval, interpreting compiled BEAM instructions with an emulator written in Erlang, and executing compiled BEAM on the BEAM VM itself. For most programs these execution modes agree, but exact equivalence breaks down at a few places that matter directly to decompilers, symbolic evaluators, refactoring tools, and alternative runtime implementations.
We study four such places in detail: binary pattern matching, fun values, selective receive, and exception metadata such as stack traces and line numbers. Our aim is not merely to catalogue awkward corner cases, but to separate what can already be reproduced exactly in plain Erlang from what still depends on BEAM-specific support or modest language/runtime extensions. Along the way we recover direct Erlang equivalents for non-trivial binary encodings, explain the evaluator's closure-adaptation problem at the arity limit, analyze why selective receive remains the most BEAM-specific construct, and identify the state that must be preserved if an Erlang-level emulator is to present compiled-BEAM behavior faithfully. The result is a more comprehensive boundary map of emulation completeness for Erlang.
Article Search
Article: icfpws26erlangmain-p5-p doi:10.1145/3830434.3830941
Erlang '26: "EMoL: Erlang Messaging and ..."
EMoL: Erlang Messaging and Monitoring over LoRa
Daniel Ferenczi, Gergely Ruda, and Melinda Tóth
(Eötvös Loránd University, Hungary; evosoft Hungary, Hungary)
Devices on the IoT edge are often low-powered microcontrollers deployed to remote locations. These devices often lack communication options, such as a TCP/IP stack, needed for Erlang features like distributed messaging or monitoring. In this paper, we present EMoL, a library we developed for cross-node messaging and monitoring of nodes communicating over the LoRa (Long Range) communication technology. EMoL offers interfaces similar to Erlang’s erlang:send/2 and erlang:monitor_node/2 functions. This comparability simplifies the use of the software architecture of regular applications to build LoRa-based distributed systems. We demonstrate that EMoL helps build distributed, reliable systems for embedded devices using a fault-tolerant leader-election algorithm.
Article Search
Article: icfpws26erlangmain-p7-p doi:10.1145/3830434.3830943
Erlang '26: "Set-Theoretic Type Checking ..."
Set-Theoretic Type Checking of Beginner Erlang Code: A Retrospective Study
Albert Schimpf, Stefan Wehr, and Annette Bieniusa
(RPTU University of Kaiserslautern-Landau, Germany; Offenburg University of Applied Sciences, Germany)
Erlang’s tooling ecosystem traditionally prioritizes flexibility over strict static guarantees, often leaving programming mistakes undetected until runtime. This is particularly acute in educational settings, where students accustomed to statically typed languages expect compiler-like feedback. Etylizer, a static type checker based on set-theoretic types, aims to provide stronger guarantees, but has mainly been evaluated on mature, idiomatic code. We present a retrospective study of student Erlang projects collected over five years to assess Etylizer’s behavior on novice-written code. Although only 14% of student functions carry type specifications, Etylizer still finds bugs in unannotated code.
The study also revealed that Etylizer’s exhaustiveness check spuriously rejects a class of otherwise well-typed programs: if-expressions that encode exhaustiveness in complementary comparison guards instead of ending in Erlang’s idiomatic catch-all true clause—a shape that community style guides discourage, that is rare in production code, but that beginners use markedly more often. We refined Etylizer’s type system to properly handle such programs. Evaluation on student and open-source projects shows that this refinement addresses spurious exhaustiveness rejections of the shape observed in the corpus. Our findings demonstrate that educational code can reveal limitations hidden in expert-oriented codebases and provide valuable insights for improving practical static analysis tools.
Article Search
Article: icfpws26erlangmain-p9-p doi:10.1145/3830434.3830945
Erlang '26: "Modern Erlang Teaching from ..."
Modern Erlang Teaching from Code Refactoring to Actor System Verification
Sergey Staroletov
(Polzunov Altai State Technical University, Russian Federation)
This paper summarizes the author's many years of experience teaching the functional Erlang language in the Master's program "Software Engineering". Original methodological techniques aimed at bridging the cognitive gap in the transition from imperative to functional thinking are presented. In particular, the following are considered in detail: systematic refactoring of imperative code into functional code by eliminating sequential operators ("commas"); the use of recursive Taylor series decomposition as an exercise that changes students' understanding of recursion; a comparison of the declarative style of Erlang with pattern matching and Java code overloaded with object transformations via JInterface; a demonstration of lightweight processes using the example of a TCP server that withstands a huge number of connections on weak hardware, with a brief comparison to modern Java virtual threads; a case study of a simplified model of the PoET consensus protocol; verification of actor models in the Promela language as a logical continuation of the study of actors; and an end-to-end approach to laboratory work, in which students sequentially develop a single distributed system from simple processes to OTP supervision, Java integration, verification, and optional porting to Cloud Haskell. The paper also discusses how the course addresses the challenges posed by generative AI in programming education, emphasising live coding and incremental code construction as a countermeasure to over-reliance on AI-generated code.
Article Search
Article: icfpws26erlangmain-p11-p doi:10.1145/3830434.3830946
Erlang '26: "Green Benchmarking of BEAM ..."
Green Benchmarking of BEAM Languages
Youssef Gharbi, István Bozó, and Melinda Tóth
(Eötvös Loránd University, Hungary)
Backend services run continuously, which makes energy use an important part of software design. This paper presents measurements from our benchmark framework for web servers running on the Erlang virtual machine. We compare Erlang, Elixir, and Gleam software using several web server frameworks under static, dynamic, and WebSocket workloads. Green software research shows that sustainability must be addressed at the application layer. Our results extend this view to BEAM web stacks under controlled load. The measurements reveal clear differences between languages and frameworks, with some stacks keeping stable throughput and lower energy under stress, while others show longer runtimes or reduced success.
Article Search
Article: icfpws26erlangmain-p6-p doi:10.1145/3830434.3830942
Erlang '26: "Towards Exact Semantic Equivalence ..."
Towards Exact Semantic Equivalence of Erlang BEAM Constructs: Lessons from Advanced Emulation and Decompilation
Gregory Morse and Melinda Tóth
(Eötvös Loránd University, Hungary)
Erlang offers three practically relevant ways to run code: evaluating abstract syntax trees with erl_eval, interpreting compiled BEAM instructions with an emulator written in Erlang, and executing compiled BEAM on the BEAM VM itself. For most programs these execution modes agree, but exact equivalence breaks down at a few places that matter directly to decompilers, symbolic evaluators, refactoring tools, and alternative runtime implementations.
We study four such places in detail: binary pattern matching, fun values, selective receive, and exception metadata such as stack traces and line numbers. Our aim is not merely to catalogue awkward corner cases, but to separate what can already be reproduced exactly in plain Erlang from what still depends on BEAM-specific support or modest language/runtime extensions. Along the way we recover direct Erlang equivalents for non-trivial binary encodings, explain the evaluator's closure-adaptation problem at the arity limit, analyze why selective receive remains the most BEAM-specific construct, and identify the state that must be preserved if an Erlang-level emulator is to present compiled-BEAM behavior faithfully. The result is a more comprehensive boundary map of emulation completeness for Erlang.
Article Search
Article: icfpws26erlangmain-p5-p doi:10.1145/3830434.3830941
Erlang '26: "EMoL: Erlang Messaging and ..."
EMoL: Erlang Messaging and Monitoring over LoRa
Daniel Ferenczi, Gergely Ruda, and Melinda Tóth
(Eötvös Loránd University, Hungary; evosoft Hungary, Hungary)
Devices on the IoT edge are often low-powered microcontrollers deployed to remote locations. These devices often lack communication options, such as a TCP/IP stack, needed for Erlang features like distributed messaging or monitoring. In this paper, we present EMoL, a library we developed for cross-node messaging and monitoring of nodes communicating over the LoRa (Long Range) communication technology. EMoL offers interfaces similar to Erlang’s erlang:send/2 and erlang:monitor_node/2 functions. This comparability simplifies the use of the software architecture of regular applications to build LoRa-based distributed systems. We demonstrate that EMoL helps build distributed, reliable systems for embedded devices using a fault-tolerant leader-election algorithm.
Article Search
Article: icfpws26erlangmain-p7-p doi:10.1145/3830434.3830943
Erlang '26: "Set-Theoretic Type Checking ..."
Set-Theoretic Type Checking of Beginner Erlang Code: A Retrospective Study
Albert Schimpf, Stefan Wehr, and Annette Bieniusa
(RPTU University of Kaiserslautern-Landau, Germany; Offenburg University of Applied Sciences, Germany)
Erlang’s tooling ecosystem traditionally prioritizes flexibility over strict static guarantees, often leaving programming mistakes undetected until runtime. This is particularly acute in educational settings, where students accustomed to statically typed languages expect compiler-like feedback. Etylizer, a static type checker based on set-theoretic types, aims to provide stronger guarantees, but has mainly been evaluated on mature, idiomatic code. We present a retrospective study of student Erlang projects collected over five years to assess Etylizer’s behavior on novice-written code. Although only 14% of student functions carry type specifications, Etylizer still finds bugs in unannotated code.
The study also revealed that Etylizer’s exhaustiveness check spuriously rejects a class of otherwise well-typed programs: if-expressions that encode exhaustiveness in complementary comparison guards instead of ending in Erlang’s idiomatic catch-all true clause—a shape that community style guides discourage, that is rare in production code, but that beginners use markedly more often. We refined Etylizer’s type system to properly handle such programs. Evaluation on student and open-source projects shows that this refinement addresses spurious exhaustiveness rejections of the shape observed in the corpus. Our findings demonstrate that educational code can reveal limitations hidden in expert-oriented codebases and provide valuable insights for improving practical static analysis tools.
Article Search
Article: icfpws26erlangmain-p9-p doi:10.1145/3830434.3830945