RT Journal Article
T1 Deriving overloaded success type schemes in Erlang
A1 López Fraguas, Francisco Javier
A1 Montenegro Montes, Manuel
A1 Suárez García, Gorka
AB Erlang 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.
PB Elsevier
SN 2590-1184
YR 2020
FD 2020-03-19
LK https://hdl.handle.net/20.500.14352/7067
UL https://hdl.handle.net/20.500.14352/7067
LA eng
NO Ministerio de Economía y Competitividad (MINECO)
NO Comunidad de Madrid/FEDER
DS Docta Complutense
RD 10 abr 2025