Erlang's dynamic typing discipline can lead to runtime errors that persist even after process restarts. Some of these runtime errors could be prevented through static type checking. While Erlang provides a type specification language, the compiler does not enforce these types, thereby limiting their role to documentation purposes. Type checking Erlang code is challenging due to language features such as dynamic type tests, subtyping, equi-recursive types, polymorphism, intersection types in signatures, and untagged union types. This work presents a set-theoretic type system for Erlang which captures the core features of Erlang's existing type language. The formal type system guarantees type soundness, and ensures that type checking remains decidable. Additionally, an implementation of a type checker is provided, supporting all features of the Erlang type language and most term-level language constructs. A case study with modules from Erlang's standard library, an external project, and the type checker itself demonstrates its effectiveness in verifying real-world Erlang code.

翻译：Erlang的动态类型机制可能导致进程重启后仍持续存在的运行时错误。部分此类运行时错误可通过静态类型检查加以防范。尽管Erlang提供了类型规格语言，但编译器并不强制实施这些类型，致使其功能仅局限于文档说明。由于语言特性包含动态类型测试、子类型化、等递归类型、多态性、签名中的交集类型以及无标签联合类型，对Erlang代码进行类型检查极具挑战性。本研究提出一种面向Erlang的集合论类型系统，该体系能够涵盖Erlang现有类型语言的核心特性。该形式化类型系统保证了类型健全性，并确保类型检查保持可判定性。此外，本研究还实现了一个类型检查器，支持Erlang类型语言的全部特性及大部分术语级语言构造。通过对Erlang标准库模块、外部项目及类型检查器自身进行的案例研究，验证了该方案在检测实际Erlang代码中的有效性。