López Fraguas, Francisco JavierMontenegro Montes, ManuelSuárez García, Gorka2023-06-172023-06-172020-03-192590-118410.1016/j.cola.2020.100965https://hdl.handle.net/20.500.14352/7067Erlang is a programming language which brings together the features of functional programming and actor-based concurrency. Although it is a dynamically-typed language, there exists a tool (Dialyzer) that analyses Erlang programs in order to detect type discrepancies at compile-time. This tool is based on the notion of success types, which are overapproximations to the actual semantics of expressions, so that the evaluation of an ‘ill-typed’ expression will eventually fail at runtime. Dialyzer allows programmers to provide their own type specifications. Although such specifications can be polymorphic and overloaded (i.e., reflecting different executing branches) for documentation purposes, the type analysis disregards the information provided by polymorphic type schemes and so does, in some cases, with overloaded types. In this paper we introduce: (1) a type system that allows us to obtain polymorphic overloaded success type schemes for programs, (2) a semantic definition of this kind of types, and (3) correctness results that prove that the adequacy of the obtained types w.r.t. the semantics of expressions.engAtribución-NoComercial-SinDerivadas 3.0 Españahttps://creativecommons.org/licenses/by-nc-nd/3.0/es/journal articlehttps://doi.org/10.1016/j.cola.2020.100965open accesspolymorphic typestype systemsErlangsuccess typesprogram semanticstipos polimórficossistemas de tipossemántica de programasLenguajes de programaciónProgramación de ordenadores (Informática)Software1203.23 Lenguajes de Programación1203.23 Lenguajes de Programación3304.16 Diseño Lógico