Fri 28 Aug 2026 11:30 - 12:00 at IP139 Kelley - Types and Semantics

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 \texttt{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.

Fri 28 Aug

Displayed time zone: Eastern Time (US & Canada) change

11:00 - 12:30
Types and SemanticsErlang at IP139 Kelley
11:00
30m
Talk
A Mechanised Semantics of Erlang’s ReferencesRemote
Erlang
Dániel Lukács 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
Link to publication DOI File Attached
11:30
30m
Talk
Set-Theoretic Type Checking of Beginner Erlang Code: A Retrospective StudyRemote
Erlang
Albert Schimpf University of Kaiserslautern-Landau, Stefan Wehr Offenburg University of Applied Sciences, Annette Bieniusa RPTU Kaiserslautern-Landau
DOI
12:00
30m
Talk
Towards Exact Semantic Equivalence of Erlang BEAM Constructs: Lessons from Advanced Emulation and DecompilationRemote
Erlang
Gregory Morse Eötvös Loránd University (ELTE), Melinda Tóth Eötvös Loránd University
Link to publication DOI File Attached