Erlang '24: "Unsafe Impedance: Safe Languages ..."
Unsafe Impedance: Safe Languages and Safe by Design Software
Lee Barney and Adolfo Neto
(Brigham Young University-Idaho, USA; Federal University of Technology Paraná, Brazil)
In December 2023, security agencies from five countries in North America, Europe, and the south Pacific produced a document encouraging senior executives in all software pro- ducing organizations to take responsibility for and oversight of the security of the software their organizations produce. In February 2024, the White House released a cybersecurity outline, highlighting the December document. In this work we review the safe languages listed in these documents, and compare the safety of those languages with Erlang and Elixir, two BEAM languages. These security agencies’ declaration of some languages as safe is necessary but insufficient to make wise decisions regarding what language to use when creating code. We propose an additional way of looking at languages and the ease with which unsafe code can be written and used. We call this new perspective unsafe impedance. We then go on to use unsafe impedance to examine nine languages that are considered to be safe. Finally, we suggest that business processes include what we refer to as an Unsafe Acceptance Process. This Unsafe Acceptance Process can be used as part of the memory safe roadmaps suggested by these agencies. Unsafe Acceptance Processes can aid organizations in their production of safe by design software.
@InProceedings{Erlang24p76,
author = {Lee Barney and Adolfo Neto},
title = {Unsafe Impedance: Safe Languages and Safe by Design Software},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {76-83},
doi = {10.1145/3677995.3678196},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p77-p doi:10.1145/3677995.3678196
Erlang '24: "Controlled Scheduling of Concurrent ..."
Controlled Scheduling of Concurrent Elixir Programs
Luis Eduardo Bueso de Barrio, Lars-Åke Fredlund, Clara Benac Earle, Ángel Herranz, and Julio Mariño
(Universidad Politécnica de Madrid, Spain)
We describe the design and implementation of Scheduler, a new library for Elixir which provides a user-level scheduler. The goal is to improve the control over scheduling decisions, i.e., which process runs at which time, in order to obtain executions that are more random, but which are also repeatable and modifiable, and which moreover provide a detailed explanation of the scheduling decisions taken. This work is inspired by the Pulse user-level scheduler for Erlang programs, as well as other related tools. Our library is agnostic regarding what other testing/execution/formal verification tool uses the scheduler, and instruments Elixir code running under the scheduler through use of the Elixir macro facility. Moreover, the library provides a number of algorithms to explore the state space of the concurrent programs under study, including random search, depth-first search (potentially capable of exploring the whole state space of the program-under-study), and a novel search algorithm which selects schedules randomly. As an example the Scheduler library is applied to the task of checking whether a number of snapshot algorithms are correct.
@InProceedings{Erlang24p67,
author = {Luis Eduardo Bueso de Barrio and Lars-Åke Fredlund and Clara Benac Earle and Ángel Herranz and Julio Mariño},
title = {Controlled Scheduling of Concurrent Elixir Programs},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {67-75},
doi = {10.1145/3677995.3678195},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p62-p doi:10.1145/3677995.3678195
Erlang '24: "Same Same but Different: A ..."
Same Same but Different: A Comparative Analysis of Static Type Checkers in Erlang
Florian Berger, Albert Schimpf, Annette Bieniusa, and Stefan Wehr
(University of Kaiserslautern-Landau, Germany; Offenburg University of Applied Sciences, Germany)
Erlang is a dynamically typed language with support for optional type annotations. Though Erlang’s type annotations were originally intended for documentation, static analysis tools soon utilized them for semantic checks. The most advanced and mature of these tools is Dialyzer, a success typing-based tool widely used in current projects. Attempts to retrofit a static type system employing the type annotations have so far remained in the realm of research prototypes. Recently, three further tools have been developed: Gradualizer, eqWAlizer, and Etylizer. But, due to a need for more semantic agreement on Erlang’s type annotations, their results differ in ways that can be challenging for users to interpret. In this paper, we cross-compare the state-of-the-art static checkers regarding their expressivity and performance on the union of their respective test suites. Unsurprisingly, we find that the tools perform best on their own test suites. While Gradualizer, Etylizer, and eqWAlizer disagree on 25% - 45% of test cases across all test suites, Dialyzer’s success-typing approach sets it apart in its interpretation of the type annotations. Our analysis emphasizes that the nature of Erlang’s type language remains challenging when it comes to develop a correct and efficient static type checker.
@InProceedings{Erlang24p2,
author = {Florian Berger and Albert Schimpf and Annette Bieniusa and Stefan Wehr},
title = {Same Same but Different: A Comparative Analysis of Static Type Checkers in Erlang},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {2-12},
doi = {10.1145/3677995.3678189},
year = {2024},
}
Publisher's Version
Info
Article: icfpws24erlangmain-p1-p doi:10.1145/3677995.3678189
Erlang '24: "Erla⁺: Translating TLA⁺ ..."
Erla⁺: Translating TLA⁺ Models into Executable Actor-Based Implementations
Marian Hristov and Annette Bieniusa
(University of Kaiserslautern-Landau, Germany)
Distributed systems are notoriously difficult to design and implement correctly. Although formal methods provide rigorous approaches to verifying the adherence of a program to its specification, there still exists a gap between a formal model and implementation if the model and its implementation are only loosely coupled. Developers usually overcome this gap through manual effort, which may result in the introduction of unexpected bugs. In this paper, we present Erla+, a translator which automatically translates models written in a subset of the PlusCal language to TLA+ for formal reasoning and produces executable Erlang programs in one run. Erla+ additionally provides new PlusCal primitives for actor-style modeling, thus clearly separating the modeled system from its environment. We show the expressivity and strengths of Erla+ by applying it to representative use cases such as a Raft-based key-value store. Our evaluation shows that the implementations generated by Erla+ offer competitive performance against manually written and optimized state-of-the-art libraries.
@InProceedings{Erlang24p13,
author = {Marian Hristov and Annette Bieniusa},
title = {Erla⁺: Translating TLA⁺ Models into Executable Actor-Based Implementations},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {13-23},
doi = {10.1145/3677995.3678190},
year = {2024},
}
Publisher's Version
Info
Article: icfpws24erlangmain-p12-p doi:10.1145/3677995.3678190
Erlang '24: "Same Same but Different: A ..."
Same Same but Different: A Comparative Analysis of Static Type Checkers in Erlang
Florian Berger, Albert Schimpf, Annette Bieniusa, and Stefan Wehr
(University of Kaiserslautern-Landau, Germany; Offenburg University of Applied Sciences, Germany)
Erlang is a dynamically typed language with support for optional type annotations. Though Erlang’s type annotations were originally intended for documentation, static analysis tools soon utilized them for semantic checks. The most advanced and mature of these tools is Dialyzer, a success typing-based tool widely used in current projects. Attempts to retrofit a static type system employing the type annotations have so far remained in the realm of research prototypes. Recently, three further tools have been developed: Gradualizer, eqWAlizer, and Etylizer. But, due to a need for more semantic agreement on Erlang’s type annotations, their results differ in ways that can be challenging for users to interpret. In this paper, we cross-compare the state-of-the-art static checkers regarding their expressivity and performance on the union of their respective test suites. Unsurprisingly, we find that the tools perform best on their own test suites. While Gradualizer, Etylizer, and eqWAlizer disagree on 25% - 45% of test cases across all test suites, Dialyzer’s success-typing approach sets it apart in its interpretation of the type annotations. Our analysis emphasizes that the nature of Erlang’s type language remains challenging when it comes to develop a correct and efficient static type checker.
@InProceedings{Erlang24p2,
author = {Florian Berger and Albert Schimpf and Annette Bieniusa and Stefan Wehr},
title = {Same Same but Different: A Comparative Analysis of Static Type Checkers in Erlang},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {2-12},
doi = {10.1145/3677995.3678189},
year = {2024},
}
Publisher's Version
Info
Article: icfpws24erlangmain-p1-p doi:10.1145/3677995.3678189
Erlang '24: "Erlang on TOAST: Generating ..."
Erlang on TOAST: Generating Erlang Stubs with Inline TOAST Monitors
Jonah Pears, Laura Bocchi, and Raymond Hu
(University of Kent, United Kingdom; Queen Mary University of London, United Kingdom)
In this work, we consider the formal framework TOAST for timed asynchronous interactions featuring mixed-choice states. TOAST extends the theory of timed asynchronous session types to support modelling of communication protocols featuring timeouts, which despite being commonplace in practice were previously out of reach for session type theory. We present ongoing work towards a practical toolchain that (a) automates the generation of correct-by-construction program stubs with timeouts in Erlang from TOAST processes that implement a TOAST protocol, and (b) provides an inline monitoring framework for TOAST protocols integrated with Erlang supervisors. Our toolchain generates Erlang code with a close correspondence to the source TOAST model by building on a formal correspondence between session types and Communicating Finite State Machines. The monitoring framework can be configured to perform either runtime verification or enforcement with respect to the source protocol, ensuring communication safety.
@InProceedings{Erlang24p33,
author = {Jonah Pears and Laura Bocchi and Raymond Hu},
title = {Erlang on TOAST: Generating Erlang Stubs with Inline TOAST Monitors},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {33-44},
doi = {10.1145/3677995.3678192},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p22-p doi:10.1145/3677995.3678192
Erlang '24: "Controlled Scheduling of Concurrent ..."
Controlled Scheduling of Concurrent Elixir Programs
Luis Eduardo Bueso de Barrio, Lars-Åke Fredlund, Clara Benac Earle, Ángel Herranz, and Julio Mariño
(Universidad Politécnica de Madrid, Spain)
We describe the design and implementation of Scheduler, a new library for Elixir which provides a user-level scheduler. The goal is to improve the control over scheduling decisions, i.e., which process runs at which time, in order to obtain executions that are more random, but which are also repeatable and modifiable, and which moreover provide a detailed explanation of the scheduling decisions taken. This work is inspired by the Pulse user-level scheduler for Erlang programs, as well as other related tools. Our library is agnostic regarding what other testing/execution/formal verification tool uses the scheduler, and instruments Elixir code running under the scheduler through use of the Elixir macro facility. Moreover, the library provides a number of algorithms to explore the state space of the concurrent programs under study, including random search, depth-first search (potentially capable of exploring the whole state space of the program-under-study), and a novel search algorithm which selects schedules randomly. As an example the Scheduler library is applied to the task of checking whether a number of snapshot algorithms are correct.
@InProceedings{Erlang24p67,
author = {Luis Eduardo Bueso de Barrio and Lars-Åke Fredlund and Clara Benac Earle and Ángel Herranz and Julio Mariño},
title = {Controlled Scheduling of Concurrent Elixir Programs},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {67-75},
doi = {10.1145/3677995.3678195},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p62-p doi:10.1145/3677995.3678195
Erlang '24: "Elixir-Powered Low-Income ..."
Elixir-Powered Low-Income Animal Shelter Support: An Experience Report from Conception to Production
Carla Rodríguez Estévez and Laura M. Castro
(Universidade da Coruña, Spain)
Animal shelters are non-governmental organizations that have to face many difficulties in their management and carry out actions to help unprotected animals in the area. Apart from being small organizations and generally having limited resources, many of them also struggle with outdated tools or face challenges in centralizing their information and pro- cesses. However, the main problem faced by them is related to their economic situation and most of the time they need to use free online tools for their management. This work presents and explains a Phoenix web application solution to assist in the management of these groups, which leverages affordable development and easy maintenance with tailoring to meet their main needs. With this experience report, we aim to demonstrate that BEAM technologies, which have already proven their effectiveness in bigger corporate set- tings, such as WhatsApp or Discord, are also well-suited for smaller and more modest environments. Moreover, this aims to be an example of the use of Elixir/Phoenix in a non-profit environment, typical for social and community projects, with needs specific to the world in which they exist.
@InProceedings{Erlang24p96,
author = {Carla Rodríguez Estévez and Laura M. Castro},
title = {Elixir-Powered Low-Income Animal Shelter Support: An Experience Report from Conception to Production},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {96-107},
doi = {10.1145/3677995.3680402},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p88n-p doi:10.1145/3677995.3680402
Erlang '24: "The Benefits of Tierless Elixir/Potato ..."
The Benefits of Tierless Elixir/Potato for Engineering IoT Systems
Solaris Li, Phil Trinder, Christophe De Troyer, Mart Lubbers, and Adrian Ramsingh
(University of Glasgow, United Kingdom; Vrije Universiteit Brussel, Belgium; Radboud University Nijmegen, Netherlands; Sia Fusion, United Kingdom)
IoT systems are increasingly pervasive, and developing, maintaining and ensuring the reliability of the software is challenging. IoT software is conventionally structured in multiple distributed tiers, where tiers use different programming languages and components that must interoperate. One way to minimise this complexity is to use a single tierless language to specify the entire IoT system. Tierless IoT languages require extremely sophisticated implementations, and are new and rare. A previous study compared two Clean-based tierless implementations of a smart campus IoT system (CRS and CWS) with two conventional tiered Python implementations (PRS and PWS). It showed that tierless languages dramatically reduce development effort. This paper describes a new implementation of the smart campus system in the Elixir/Potato tierless language (ERS), and compares ERS with the other implementations to show the following. (1) We provide further evidence that using a tierless IoT language reduces development effort. (2) We provide the first ever comparative study of two fundamentally different tierless IoT languages, i.e. we compare Elixir/Potato with Clean/iTask(mTask) using the ERS and CRS/CWS case studies. (3) We provide the first ever analysis of the software engineering costs of providing failure management in a tierless IoT language.
@InProceedings{Erlang24p84,
author = {Solaris Li and Phil Trinder and Christophe De Troyer and Mart Lubbers and Adrian Ramsingh},
title = {The Benefits of Tierless Elixir/Potato for Engineering IoT Systems},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {84-95},
doi = {10.1145/3677995.3678197},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p79-p doi:10.1145/3677995.3678197
Erlang '24: "Nominal Types for Erlang ..."
Nominal Types for Erlang
Isabell Huang, John Högberg, Kiko Fernandez-Reyes, and Tobias Wrigstad
(Ericsson, Sweden; Uppsala University, Sweden)
Erlang is a functional programming language with structural type-checking. Opaque types are the only types with a nominal component, where their names are used for type-checking. Using opaque types for nominal typing is possible, but it limits the use of pattern-matching and deconstruction to the module where it is defined. To distinguish types by names without imposing extra constraints, we introduce the new concept of nominal types for Erlang, together with a well-tested type-checking implementation in Dialyzer. We define a new syntax for declaring nominal types and a set of rules that specify how nominal types should be type-checked with respect to other nominal types and non-nominal types, which is designed to ensure backwards compatibility. Nominal type-checking is implemented on top of Dialyzer's structural type-checking logic. Through testing in the Erlang/OTP codebase, we show that nominal types can encode Erlang's opaque types, thereby improving Dialyzer's performance and maintainability.
@InProceedings{Erlang24p24,
author = {Isabell Huang and John Högberg and Kiko Fernandez-Reyes and Tobias Wrigstad},
title = {Nominal Types for Erlang},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {24-32},
doi = {10.1145/3677995.3678191},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p16-p doi:10.1145/3677995.3678191
Erlang '24: "Controlled Scheduling of Concurrent ..."
Controlled Scheduling of Concurrent Elixir Programs
Luis Eduardo Bueso de Barrio, Lars-Åke Fredlund, Clara Benac Earle, Ángel Herranz, and Julio Mariño
(Universidad Politécnica de Madrid, Spain)
We describe the design and implementation of Scheduler, a new library for Elixir which provides a user-level scheduler. The goal is to improve the control over scheduling decisions, i.e., which process runs at which time, in order to obtain executions that are more random, but which are also repeatable and modifiable, and which moreover provide a detailed explanation of the scheduling decisions taken. This work is inspired by the Pulse user-level scheduler for Erlang programs, as well as other related tools. Our library is agnostic regarding what other testing/execution/formal verification tool uses the scheduler, and instruments Elixir code running under the scheduler through use of the Elixir macro facility. Moreover, the library provides a number of algorithms to explore the state space of the concurrent programs under study, including random search, depth-first search (potentially capable of exploring the whole state space of the program-under-study), and a novel search algorithm which selects schedules randomly. As an example the Scheduler library is applied to the task of checking whether a number of snapshot algorithms are correct.
@InProceedings{Erlang24p67,
author = {Luis Eduardo Bueso de Barrio and Lars-Åke Fredlund and Clara Benac Earle and Ángel Herranz and Julio Mariño},
title = {Controlled Scheduling of Concurrent Elixir Programs},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {67-75},
doi = {10.1145/3677995.3678195},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p62-p doi:10.1145/3677995.3678195
Erlang '24: "Controlled Scheduling of Concurrent ..."
Controlled Scheduling of Concurrent Elixir Programs
Luis Eduardo Bueso de Barrio, Lars-Åke Fredlund, Clara Benac Earle, Ángel Herranz, and Julio Mariño
(Universidad Politécnica de Madrid, Spain)
We describe the design and implementation of Scheduler, a new library for Elixir which provides a user-level scheduler. The goal is to improve the control over scheduling decisions, i.e., which process runs at which time, in order to obtain executions that are more random, but which are also repeatable and modifiable, and which moreover provide a detailed explanation of the scheduling decisions taken. This work is inspired by the Pulse user-level scheduler for Erlang programs, as well as other related tools. Our library is agnostic regarding what other testing/execution/formal verification tool uses the scheduler, and instruments Elixir code running under the scheduler through use of the Elixir macro facility. Moreover, the library provides a number of algorithms to explore the state space of the concurrent programs under study, including random search, depth-first search (potentially capable of exploring the whole state space of the program-under-study), and a novel search algorithm which selects schedules randomly. As an example the Scheduler library is applied to the task of checking whether a number of snapshot algorithms are correct.
@InProceedings{Erlang24p67,
author = {Luis Eduardo Bueso de Barrio and Lars-Åke Fredlund and Clara Benac Earle and Ángel Herranz and Julio Mariño},
title = {Controlled Scheduling of Concurrent Elixir Programs},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {67-75},
doi = {10.1145/3677995.3678195},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p62-p doi:10.1145/3677995.3678195
Erlang '24: "Nominal Types for Erlang ..."
Nominal Types for Erlang
Isabell Huang, John Högberg, Kiko Fernandez-Reyes, and Tobias Wrigstad
(Ericsson, Sweden; Uppsala University, Sweden)
Erlang is a functional programming language with structural type-checking. Opaque types are the only types with a nominal component, where their names are used for type-checking. Using opaque types for nominal typing is possible, but it limits the use of pattern-matching and deconstruction to the module where it is defined. To distinguish types by names without imposing extra constraints, we introduce the new concept of nominal types for Erlang, together with a well-tested type-checking implementation in Dialyzer. We define a new syntax for declaring nominal types and a set of rules that specify how nominal types should be type-checked with respect to other nominal types and non-nominal types, which is designed to ensure backwards compatibility. Nominal type-checking is implemented on top of Dialyzer's structural type-checking logic. Through testing in the Erlang/OTP codebase, we show that nominal types can encode Erlang's opaque types, thereby improving Dialyzer's performance and maintainability.
@InProceedings{Erlang24p24,
author = {Isabell Huang and John Högberg and Kiko Fernandez-Reyes and Tobias Wrigstad},
title = {Nominal Types for Erlang},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {24-32},
doi = {10.1145/3677995.3678191},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p16-p doi:10.1145/3677995.3678191
Erlang '24: "Modeling Erlang Compiler IR ..."
Modeling Erlang Compiler IR as SMT Formulas
John Högberg
(Ericsson, Sweden)
Erlang is an unorthodox language that has fault-tolerance and observability (tracing) baked into the language. This allows users to debug production systems without the maintenance overhead of adding these features manually, but comes at the cost of adding a side effect to almost every operation. Because the design choices around tracing err on the side of maximum observability, the compiler does not have much freedom to perform common optimizations, and requires sophisticated analysis to safely apply all but the simplest transformations. Each individual optimization also implements its own bespoke analysis, which is error-prone and difficult to maintain. This report describes an ongoing experiment on translating one of the compiler's intermediate representations (IR) to formulas, enabling the use of a satisfiability modulo theories (SMT) solver to drive analysis as well as prove the semantics-preserving nature of optimizations.
@InProceedings{Erlang24p45,
author = {John Högberg},
title = {Modeling Erlang Compiler IR as SMT Formulas},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {45-54},
doi = {10.1145/3677995.3678193},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p24-p doi:10.1145/3677995.3678193
Erlang '24: "Is This Really a Refactoring? ..."
Is This Really a Refactoring? Automated Equivalence Checking for Erlang Projects
Bendegúz Seres, Dániel Horpácsi, and Simon Thompson
(Eötvös Loránd University, Hungary; University of Kent, United Kingdom)
We present an automated approach to checking whether a change to a repository is a refactoring, that is, it makes no change to the behaviour of the system. This is implemented in the EquivcheckEr tool, which detects the places in which the code has changed, and compares the old and new versions of all functions that are affected by the change, applying the functions to randomly generated inputs. Our tool works for projects written in Erlang, and so needs to deal with effectful as well as pure functions. We aim only to report inequivalence when we have concrete evidence to that effect, avoiding any "false positive" counterexamples.
@InProceedings{Erlang24p55,
author = {Bendegúz Seres and Dániel Horpácsi and Simon Thompson},
title = {Is This Really a Refactoring? Automated Equivalence Checking for Erlang Projects},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {55-66},
doi = {10.1145/3677995.3678194},
year = {2024},
}
Publisher's Version
Info
Article: icfpws24erlangmain-p50-p doi:10.1145/3677995.3678194
Erlang '24: "Erla⁺: Translating TLA⁺ ..."
Erla⁺: Translating TLA⁺ Models into Executable Actor-Based Implementations
Marian Hristov and Annette Bieniusa
(University of Kaiserslautern-Landau, Germany)
Distributed systems are notoriously difficult to design and implement correctly. Although formal methods provide rigorous approaches to verifying the adherence of a program to its specification, there still exists a gap between a formal model and implementation if the model and its implementation are only loosely coupled. Developers usually overcome this gap through manual effort, which may result in the introduction of unexpected bugs. In this paper, we present Erla+, a translator which automatically translates models written in a subset of the PlusCal language to TLA+ for formal reasoning and produces executable Erlang programs in one run. Erla+ additionally provides new PlusCal primitives for actor-style modeling, thus clearly separating the modeled system from its environment. We show the expressivity and strengths of Erla+ by applying it to representative use cases such as a Raft-based key-value store. Our evaluation shows that the implementations generated by Erla+ offer competitive performance against manually written and optimized state-of-the-art libraries.
@InProceedings{Erlang24p13,
author = {Marian Hristov and Annette Bieniusa},
title = {Erla⁺: Translating TLA⁺ Models into Executable Actor-Based Implementations},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {13-23},
doi = {10.1145/3677995.3678190},
year = {2024},
}
Publisher's Version
Info
Article: icfpws24erlangmain-p12-p doi:10.1145/3677995.3678190
Erlang '24: "Erlang on TOAST: Generating ..."
Erlang on TOAST: Generating Erlang Stubs with Inline TOAST Monitors
Jonah Pears, Laura Bocchi, and Raymond Hu
(University of Kent, United Kingdom; Queen Mary University of London, United Kingdom)
In this work, we consider the formal framework TOAST for timed asynchronous interactions featuring mixed-choice states. TOAST extends the theory of timed asynchronous session types to support modelling of communication protocols featuring timeouts, which despite being commonplace in practice were previously out of reach for session type theory. We present ongoing work towards a practical toolchain that (a) automates the generation of correct-by-construction program stubs with timeouts in Erlang from TOAST processes that implement a TOAST protocol, and (b) provides an inline monitoring framework for TOAST protocols integrated with Erlang supervisors. Our toolchain generates Erlang code with a close correspondence to the source TOAST model by building on a formal correspondence between session types and Communicating Finite State Machines. The monitoring framework can be configured to perform either runtime verification or enforcement with respect to the source protocol, ensuring communication safety.
@InProceedings{Erlang24p33,
author = {Jonah Pears and Laura Bocchi and Raymond Hu},
title = {Erlang on TOAST: Generating Erlang Stubs with Inline TOAST Monitors},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {33-44},
doi = {10.1145/3677995.3678192},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p22-p doi:10.1145/3677995.3678192
Erlang '24: "Nominal Types for Erlang ..."
Nominal Types for Erlang
Isabell Huang, John Högberg, Kiko Fernandez-Reyes, and Tobias Wrigstad
(Ericsson, Sweden; Uppsala University, Sweden)
Erlang is a functional programming language with structural type-checking. Opaque types are the only types with a nominal component, where their names are used for type-checking. Using opaque types for nominal typing is possible, but it limits the use of pattern-matching and deconstruction to the module where it is defined. To distinguish types by names without imposing extra constraints, we introduce the new concept of nominal types for Erlang, together with a well-tested type-checking implementation in Dialyzer. We define a new syntax for declaring nominal types and a set of rules that specify how nominal types should be type-checked with respect to other nominal types and non-nominal types, which is designed to ensure backwards compatibility. Nominal type-checking is implemented on top of Dialyzer's structural type-checking logic. Through testing in the Erlang/OTP codebase, we show that nominal types can encode Erlang's opaque types, thereby improving Dialyzer's performance and maintainability.
@InProceedings{Erlang24p24,
author = {Isabell Huang and John Högberg and Kiko Fernandez-Reyes and Tobias Wrigstad},
title = {Nominal Types for Erlang},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {24-32},
doi = {10.1145/3677995.3678191},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p16-p doi:10.1145/3677995.3678191
Erlang '24: "The Benefits of Tierless Elixir/Potato ..."
The Benefits of Tierless Elixir/Potato for Engineering IoT Systems
Solaris Li, Phil Trinder, Christophe De Troyer, Mart Lubbers, and Adrian Ramsingh
(University of Glasgow, United Kingdom; Vrije Universiteit Brussel, Belgium; Radboud University Nijmegen, Netherlands; Sia Fusion, United Kingdom)
IoT systems are increasingly pervasive, and developing, maintaining and ensuring the reliability of the software is challenging. IoT software is conventionally structured in multiple distributed tiers, where tiers use different programming languages and components that must interoperate. One way to minimise this complexity is to use a single tierless language to specify the entire IoT system. Tierless IoT languages require extremely sophisticated implementations, and are new and rare. A previous study compared two Clean-based tierless implementations of a smart campus IoT system (CRS and CWS) with two conventional tiered Python implementations (PRS and PWS). It showed that tierless languages dramatically reduce development effort. This paper describes a new implementation of the smart campus system in the Elixir/Potato tierless language (ERS), and compares ERS with the other implementations to show the following. (1) We provide further evidence that using a tierless IoT language reduces development effort. (2) We provide the first ever comparative study of two fundamentally different tierless IoT languages, i.e. we compare Elixir/Potato with Clean/iTask(mTask) using the ERS and CRS/CWS case studies. (3) We provide the first ever analysis of the software engineering costs of providing failure management in a tierless IoT language.
@InProceedings{Erlang24p84,
author = {Solaris Li and Phil Trinder and Christophe De Troyer and Mart Lubbers and Adrian Ramsingh},
title = {The Benefits of Tierless Elixir/Potato for Engineering IoT Systems},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {84-95},
doi = {10.1145/3677995.3678197},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p79-p doi:10.1145/3677995.3678197
Erlang '24: "The Benefits of Tierless Elixir/Potato ..."
The Benefits of Tierless Elixir/Potato for Engineering IoT Systems
Solaris Li, Phil Trinder, Christophe De Troyer, Mart Lubbers, and Adrian Ramsingh
(University of Glasgow, United Kingdom; Vrije Universiteit Brussel, Belgium; Radboud University Nijmegen, Netherlands; Sia Fusion, United Kingdom)
IoT systems are increasingly pervasive, and developing, maintaining and ensuring the reliability of the software is challenging. IoT software is conventionally structured in multiple distributed tiers, where tiers use different programming languages and components that must interoperate. One way to minimise this complexity is to use a single tierless language to specify the entire IoT system. Tierless IoT languages require extremely sophisticated implementations, and are new and rare. A previous study compared two Clean-based tierless implementations of a smart campus IoT system (CRS and CWS) with two conventional tiered Python implementations (PRS and PWS). It showed that tierless languages dramatically reduce development effort. This paper describes a new implementation of the smart campus system in the Elixir/Potato tierless language (ERS), and compares ERS with the other implementations to show the following. (1) We provide further evidence that using a tierless IoT language reduces development effort. (2) We provide the first ever comparative study of two fundamentally different tierless IoT languages, i.e. we compare Elixir/Potato with Clean/iTask(mTask) using the ERS and CRS/CWS case studies. (3) We provide the first ever analysis of the software engineering costs of providing failure management in a tierless IoT language.
@InProceedings{Erlang24p84,
author = {Solaris Li and Phil Trinder and Christophe De Troyer and Mart Lubbers and Adrian Ramsingh},
title = {The Benefits of Tierless Elixir/Potato for Engineering IoT Systems},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {84-95},
doi = {10.1145/3677995.3678197},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p79-p doi:10.1145/3677995.3678197
Erlang '24: "Environmentally Sustainable ..."
Environmentally Sustainable Software and Data Architectures (Keynote)
Madeleine Malmsten
(Unaffiliated, Germany)
The rising threat of climate change is leading countries to commit to ambitious carbon-reduction goals. Concurrently, a significant portion of Fortune 500 companies are targeting carbon emission cuts by 2030. As digital integration grows, Technology represents a huge opportunity, yet, the energy footprint of software is often overlooked. Each application transaction, interaction and new data asset adds to the energy demand, making sustainable software and data practices crucial. While improving sustainability in data and software alone won’t solve climate change, with an understanding of technology’s contribution to carbon emissions, a focus on tech’s foundational elements at multiple levels can pave the way for more substantial reductions in the future: (i) Software engineers can reduce the carbon emissions from their software and data by being aware of the effects of their choices. (ii) CTOs can make environmental sustainability a non-functional requirement for all software development. (iii) Companies can incorporate the environmental effects of software as a metric when gauging the quality of a solution. The goal is to cultivate a culture that embeds environmental sustainability into standard software and data engineering practices. Now is the perfect time to start!
@InProceedings{Erlang24p1,
author = {Madeleine Malmsten},
title = {Environmentally Sustainable Software and Data Architectures (Keynote)},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {1-1},
doi = {10.1145/3677995.3689456},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-key1-p doi:10.1145/3677995.3689456
Erlang '24: "Controlled Scheduling of Concurrent ..."
Controlled Scheduling of Concurrent Elixir Programs
Luis Eduardo Bueso de Barrio, Lars-Åke Fredlund, Clara Benac Earle, Ángel Herranz, and Julio Mariño
(Universidad Politécnica de Madrid, Spain)
We describe the design and implementation of Scheduler, a new library for Elixir which provides a user-level scheduler. The goal is to improve the control over scheduling decisions, i.e., which process runs at which time, in order to obtain executions that are more random, but which are also repeatable and modifiable, and which moreover provide a detailed explanation of the scheduling decisions taken. This work is inspired by the Pulse user-level scheduler for Erlang programs, as well as other related tools. Our library is agnostic regarding what other testing/execution/formal verification tool uses the scheduler, and instruments Elixir code running under the scheduler through use of the Elixir macro facility. Moreover, the library provides a number of algorithms to explore the state space of the concurrent programs under study, including random search, depth-first search (potentially capable of exploring the whole state space of the program-under-study), and a novel search algorithm which selects schedules randomly. As an example the Scheduler library is applied to the task of checking whether a number of snapshot algorithms are correct.
@InProceedings{Erlang24p67,
author = {Luis Eduardo Bueso de Barrio and Lars-Åke Fredlund and Clara Benac Earle and Ángel Herranz and Julio Mariño},
title = {Controlled Scheduling of Concurrent Elixir Programs},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {67-75},
doi = {10.1145/3677995.3678195},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p62-p doi:10.1145/3677995.3678195
Erlang '24: "Unsafe Impedance: Safe Languages ..."
Unsafe Impedance: Safe Languages and Safe by Design Software
Lee Barney and Adolfo Neto
(Brigham Young University-Idaho, USA; Federal University of Technology Paraná, Brazil)
In December 2023, security agencies from five countries in North America, Europe, and the south Pacific produced a document encouraging senior executives in all software pro- ducing organizations to take responsibility for and oversight of the security of the software their organizations produce. In February 2024, the White House released a cybersecurity outline, highlighting the December document. In this work we review the safe languages listed in these documents, and compare the safety of those languages with Erlang and Elixir, two BEAM languages. These security agencies’ declaration of some languages as safe is necessary but insufficient to make wise decisions regarding what language to use when creating code. We propose an additional way of looking at languages and the ease with which unsafe code can be written and used. We call this new perspective unsafe impedance. We then go on to use unsafe impedance to examine nine languages that are considered to be safe. Finally, we suggest that business processes include what we refer to as an Unsafe Acceptance Process. This Unsafe Acceptance Process can be used as part of the memory safe roadmaps suggested by these agencies. Unsafe Acceptance Processes can aid organizations in their production of safe by design software.
@InProceedings{Erlang24p76,
author = {Lee Barney and Adolfo Neto},
title = {Unsafe Impedance: Safe Languages and Safe by Design Software},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {76-83},
doi = {10.1145/3677995.3678196},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p77-p doi:10.1145/3677995.3678196
Erlang '24: "Erlang on TOAST: Generating ..."
Erlang on TOAST: Generating Erlang Stubs with Inline TOAST Monitors
Jonah Pears, Laura Bocchi, and Raymond Hu
(University of Kent, United Kingdom; Queen Mary University of London, United Kingdom)
In this work, we consider the formal framework TOAST for timed asynchronous interactions featuring mixed-choice states. TOAST extends the theory of timed asynchronous session types to support modelling of communication protocols featuring timeouts, which despite being commonplace in practice were previously out of reach for session type theory. We present ongoing work towards a practical toolchain that (a) automates the generation of correct-by-construction program stubs with timeouts in Erlang from TOAST processes that implement a TOAST protocol, and (b) provides an inline monitoring framework for TOAST protocols integrated with Erlang supervisors. Our toolchain generates Erlang code with a close correspondence to the source TOAST model by building on a formal correspondence between session types and Communicating Finite State Machines. The monitoring framework can be configured to perform either runtime verification or enforcement with respect to the source protocol, ensuring communication safety.
@InProceedings{Erlang24p33,
author = {Jonah Pears and Laura Bocchi and Raymond Hu},
title = {Erlang on TOAST: Generating Erlang Stubs with Inline TOAST Monitors},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {33-44},
doi = {10.1145/3677995.3678192},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p22-p doi:10.1145/3677995.3678192
Erlang '24: "The Benefits of Tierless Elixir/Potato ..."
The Benefits of Tierless Elixir/Potato for Engineering IoT Systems
Solaris Li, Phil Trinder, Christophe De Troyer, Mart Lubbers, and Adrian Ramsingh
(University of Glasgow, United Kingdom; Vrije Universiteit Brussel, Belgium; Radboud University Nijmegen, Netherlands; Sia Fusion, United Kingdom)
IoT systems are increasingly pervasive, and developing, maintaining and ensuring the reliability of the software is challenging. IoT software is conventionally structured in multiple distributed tiers, where tiers use different programming languages and components that must interoperate. One way to minimise this complexity is to use a single tierless language to specify the entire IoT system. Tierless IoT languages require extremely sophisticated implementations, and are new and rare. A previous study compared two Clean-based tierless implementations of a smart campus IoT system (CRS and CWS) with two conventional tiered Python implementations (PRS and PWS). It showed that tierless languages dramatically reduce development effort. This paper describes a new implementation of the smart campus system in the Elixir/Potato tierless language (ERS), and compares ERS with the other implementations to show the following. (1) We provide further evidence that using a tierless IoT language reduces development effort. (2) We provide the first ever comparative study of two fundamentally different tierless IoT languages, i.e. we compare Elixir/Potato with Clean/iTask(mTask) using the ERS and CRS/CWS case studies. (3) We provide the first ever analysis of the software engineering costs of providing failure management in a tierless IoT language.
@InProceedings{Erlang24p84,
author = {Solaris Li and Phil Trinder and Christophe De Troyer and Mart Lubbers and Adrian Ramsingh},
title = {The Benefits of Tierless Elixir/Potato for Engineering IoT Systems},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {84-95},
doi = {10.1145/3677995.3678197},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p79-p doi:10.1145/3677995.3678197
Erlang '24: "Elixir-Powered Low-Income ..."
Elixir-Powered Low-Income Animal Shelter Support: An Experience Report from Conception to Production
Carla Rodríguez Estévez and Laura M. Castro
(Universidade da Coruña, Spain)
Animal shelters are non-governmental organizations that have to face many difficulties in their management and carry out actions to help unprotected animals in the area. Apart from being small organizations and generally having limited resources, many of them also struggle with outdated tools or face challenges in centralizing their information and pro- cesses. However, the main problem faced by them is related to their economic situation and most of the time they need to use free online tools for their management. This work presents and explains a Phoenix web application solution to assist in the management of these groups, which leverages affordable development and easy maintenance with tailoring to meet their main needs. With this experience report, we aim to demonstrate that BEAM technologies, which have already proven their effectiveness in bigger corporate set- tings, such as WhatsApp or Discord, are also well-suited for smaller and more modest environments. Moreover, this aims to be an example of the use of Elixir/Phoenix in a non-profit environment, typical for social and community projects, with needs specific to the world in which they exist.
@InProceedings{Erlang24p96,
author = {Carla Rodríguez Estévez and Laura M. Castro},
title = {Elixir-Powered Low-Income Animal Shelter Support: An Experience Report from Conception to Production},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {96-107},
doi = {10.1145/3677995.3680402},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p88n-p doi:10.1145/3677995.3680402
Erlang '24: "Same Same but Different: A ..."
Same Same but Different: A Comparative Analysis of Static Type Checkers in Erlang
Florian Berger, Albert Schimpf, Annette Bieniusa, and Stefan Wehr
(University of Kaiserslautern-Landau, Germany; Offenburg University of Applied Sciences, Germany)
Erlang is a dynamically typed language with support for optional type annotations. Though Erlang’s type annotations were originally intended for documentation, static analysis tools soon utilized them for semantic checks. The most advanced and mature of these tools is Dialyzer, a success typing-based tool widely used in current projects. Attempts to retrofit a static type system employing the type annotations have so far remained in the realm of research prototypes. Recently, three further tools have been developed: Gradualizer, eqWAlizer, and Etylizer. But, due to a need for more semantic agreement on Erlang’s type annotations, their results differ in ways that can be challenging for users to interpret. In this paper, we cross-compare the state-of-the-art static checkers regarding their expressivity and performance on the union of their respective test suites. Unsurprisingly, we find that the tools perform best on their own test suites. While Gradualizer, Etylizer, and eqWAlizer disagree on 25% - 45% of test cases across all test suites, Dialyzer’s success-typing approach sets it apart in its interpretation of the type annotations. Our analysis emphasizes that the nature of Erlang’s type language remains challenging when it comes to develop a correct and efficient static type checker.
@InProceedings{Erlang24p2,
author = {Florian Berger and Albert Schimpf and Annette Bieniusa and Stefan Wehr},
title = {Same Same but Different: A Comparative Analysis of Static Type Checkers in Erlang},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {2-12},
doi = {10.1145/3677995.3678189},
year = {2024},
}
Publisher's Version
Info
Article: icfpws24erlangmain-p1-p doi:10.1145/3677995.3678189
Erlang '24: "Is This Really a Refactoring? ..."
Is This Really a Refactoring? Automated Equivalence Checking for Erlang Projects
Bendegúz Seres, Dániel Horpácsi, and Simon Thompson
(Eötvös Loránd University, Hungary; University of Kent, United Kingdom)
We present an automated approach to checking whether a change to a repository is a refactoring, that is, it makes no change to the behaviour of the system. This is implemented in the EquivcheckEr tool, which detects the places in which the code has changed, and compares the old and new versions of all functions that are affected by the change, applying the functions to randomly generated inputs. Our tool works for projects written in Erlang, and so needs to deal with effectful as well as pure functions. We aim only to report inequivalence when we have concrete evidence to that effect, avoiding any "false positive" counterexamples.
@InProceedings{Erlang24p55,
author = {Bendegúz Seres and Dániel Horpácsi and Simon Thompson},
title = {Is This Really a Refactoring? Automated Equivalence Checking for Erlang Projects},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {55-66},
doi = {10.1145/3677995.3678194},
year = {2024},
}
Publisher's Version
Info
Article: icfpws24erlangmain-p50-p doi:10.1145/3677995.3678194
Erlang '24: "Is This Really a Refactoring? ..."
Is This Really a Refactoring? Automated Equivalence Checking for Erlang Projects
Bendegúz Seres, Dániel Horpácsi, and Simon Thompson
(Eötvös Loránd University, Hungary; University of Kent, United Kingdom)
We present an automated approach to checking whether a change to a repository is a refactoring, that is, it makes no change to the behaviour of the system. This is implemented in the EquivcheckEr tool, which detects the places in which the code has changed, and compares the old and new versions of all functions that are affected by the change, applying the functions to randomly generated inputs. Our tool works for projects written in Erlang, and so needs to deal with effectful as well as pure functions. We aim only to report inequivalence when we have concrete evidence to that effect, avoiding any "false positive" counterexamples.
@InProceedings{Erlang24p55,
author = {Bendegúz Seres and Dániel Horpácsi and Simon Thompson},
title = {Is This Really a Refactoring? Automated Equivalence Checking for Erlang Projects},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {55-66},
doi = {10.1145/3677995.3678194},
year = {2024},
}
Publisher's Version
Info
Article: icfpws24erlangmain-p50-p doi:10.1145/3677995.3678194
Erlang '24: "The Benefits of Tierless Elixir/Potato ..."
The Benefits of Tierless Elixir/Potato for Engineering IoT Systems
Solaris Li, Phil Trinder, Christophe De Troyer, Mart Lubbers, and Adrian Ramsingh
(University of Glasgow, United Kingdom; Vrije Universiteit Brussel, Belgium; Radboud University Nijmegen, Netherlands; Sia Fusion, United Kingdom)
IoT systems are increasingly pervasive, and developing, maintaining and ensuring the reliability of the software is challenging. IoT software is conventionally structured in multiple distributed tiers, where tiers use different programming languages and components that must interoperate. One way to minimise this complexity is to use a single tierless language to specify the entire IoT system. Tierless IoT languages require extremely sophisticated implementations, and are new and rare. A previous study compared two Clean-based tierless implementations of a smart campus IoT system (CRS and CWS) with two conventional tiered Python implementations (PRS and PWS). It showed that tierless languages dramatically reduce development effort. This paper describes a new implementation of the smart campus system in the Elixir/Potato tierless language (ERS), and compares ERS with the other implementations to show the following. (1) We provide further evidence that using a tierless IoT language reduces development effort. (2) We provide the first ever comparative study of two fundamentally different tierless IoT languages, i.e. we compare Elixir/Potato with Clean/iTask(mTask) using the ERS and CRS/CWS case studies. (3) We provide the first ever analysis of the software engineering costs of providing failure management in a tierless IoT language.
@InProceedings{Erlang24p84,
author = {Solaris Li and Phil Trinder and Christophe De Troyer and Mart Lubbers and Adrian Ramsingh},
title = {The Benefits of Tierless Elixir/Potato for Engineering IoT Systems},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {84-95},
doi = {10.1145/3677995.3678197},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p79-p doi:10.1145/3677995.3678197
Erlang '24: "Same Same but Different: A ..."
Same Same but Different: A Comparative Analysis of Static Type Checkers in Erlang
Florian Berger, Albert Schimpf, Annette Bieniusa, and Stefan Wehr
(University of Kaiserslautern-Landau, Germany; Offenburg University of Applied Sciences, Germany)
Erlang is a dynamically typed language with support for optional type annotations. Though Erlang’s type annotations were originally intended for documentation, static analysis tools soon utilized them for semantic checks. The most advanced and mature of these tools is Dialyzer, a success typing-based tool widely used in current projects. Attempts to retrofit a static type system employing the type annotations have so far remained in the realm of research prototypes. Recently, three further tools have been developed: Gradualizer, eqWAlizer, and Etylizer. But, due to a need for more semantic agreement on Erlang’s type annotations, their results differ in ways that can be challenging for users to interpret. In this paper, we cross-compare the state-of-the-art static checkers regarding their expressivity and performance on the union of their respective test suites. Unsurprisingly, we find that the tools perform best on their own test suites. While Gradualizer, Etylizer, and eqWAlizer disagree on 25% - 45% of test cases across all test suites, Dialyzer’s success-typing approach sets it apart in its interpretation of the type annotations. Our analysis emphasizes that the nature of Erlang’s type language remains challenging when it comes to develop a correct and efficient static type checker.
@InProceedings{Erlang24p2,
author = {Florian Berger and Albert Schimpf and Annette Bieniusa and Stefan Wehr},
title = {Same Same but Different: A Comparative Analysis of Static Type Checkers in Erlang},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {2-12},
doi = {10.1145/3677995.3678189},
year = {2024},
}
Publisher's Version
Info
Article: icfpws24erlangmain-p1-p doi:10.1145/3677995.3678189
Erlang '24: "Nominal Types for Erlang ..."
Nominal Types for Erlang
Isabell Huang, John Högberg, Kiko Fernandez-Reyes, and Tobias Wrigstad
(Ericsson, Sweden; Uppsala University, Sweden)
Erlang is a functional programming language with structural type-checking. Opaque types are the only types with a nominal component, where their names are used for type-checking. Using opaque types for nominal typing is possible, but it limits the use of pattern-matching and deconstruction to the module where it is defined. To distinguish types by names without imposing extra constraints, we introduce the new concept of nominal types for Erlang, together with a well-tested type-checking implementation in Dialyzer. We define a new syntax for declaring nominal types and a set of rules that specify how nominal types should be type-checked with respect to other nominal types and non-nominal types, which is designed to ensure backwards compatibility. Nominal type-checking is implemented on top of Dialyzer's structural type-checking logic. Through testing in the Erlang/OTP codebase, we show that nominal types can encode Erlang's opaque types, thereby improving Dialyzer's performance and maintainability.
@InProceedings{Erlang24p24,
author = {Isabell Huang and John Högberg and Kiko Fernandez-Reyes and Tobias Wrigstad},
title = {Nominal Types for Erlang},
booktitle = {Proc.\ Erlang},
publisher = {ACM},
pages = {24-32},
doi = {10.1145/3677995.3678191},
year = {2024},
}
Publisher's Version
Article: icfpws24erlangmain-p16-p doi:10.1145/3677995.3678191