ICFP Workshops 2020
25th ACM SIGPLAN International Conference on Functional Programming (ICFP 2020)
Powered by
Conference Publishing Consulting

19th ACM SIGPLAN International Workshop on Erlang (Erlang 2020), August 23, 2020, Virtual Event, USA

Erlang 2020 – Proceedings

Contents - Abstracts - Authors

19th ACM SIGPLAN International Workshop on Erlang (Erlang 2020)

Frontmatter

Title Page


Message from the Chairs
It is our great pleasure to welcome you to the Nineteenth ACM SIGPLAN Erlang Workshop (Erlang’20), which is once again co-located with the annual International Conference on Functional Programming (ICFP), held as a virtual event this year. The workshop continues the tradition of being a forum for presenting research efforts and experience reports on all aspects of theory, implementation, and applications of the Erlang language and BEAM-related technologies, covering topics such as functional programming, distribution, concurrency, and scalability. The Erlang model of concurrent programming has been widely emulated, for example by Akka in Scala, Java and now Swift, and a wave of exciting programming languages are being developed on top of the Erlang VM (BEAM), such as Elixir or adaptations of Clojure.
The call for papers attracted this year a total of 8 submissions, each of which were carefully reviewed by at least four program committee members. To ensure fairness and preserve the anonymity of all authors and reviewers, papers authored by PC chairs were handled out-of-band by Natalia Chechina. The reviews were handled using the HotCRP system using "tokens", a mechanism designed to keep the reviewers anonymous even from the chairs. This year, a new initiative started to team up practitioners with experienced researchers to support them in writing their first research paper. One paper emerging from such a collaboration was submitted and also accepted for publication in the standard review process. In total, the program committee accepted four long and one short paper for publication.
Additionally, the steering committee invited the founders of Avassa for a panel discussion to talk about Erlang-fuelled inventions. The discussion will be led by Johnny Winn, who is also the host of the Elixir Fountain Podcast.
Putting together Erlang’20 has been a team effort. First of all, we thank the panellists and the authors of all submitted papers for allowing us to assemble an inspiring and appealing program. We express our gratitude to all members of the program committee, who reviewed the papers in a timely manner despite the situation due to COVID-19, providing constructive criticism and suggestions for improvement. We also greatly appreciate the efforts of this year’s ICFP Chairs, led by Stephanie Weirich as General Chair, and the workshop co-chairs, Jennifer Hackett and Leonidas Lampropoulos, who diligently answered our questions and guided us through the organisational process. Special thanks go to the virtualization committee of ICFP’20 for taking care of the online meeting arrangements: your hard work makes our experiences great. We would also like to thank the members of the Erlang Workshop’s Steering Committee for their guidance and to the Ericsson OTP team for maintaining the Erlang’20 web site. Finally, we thank ACM SIGPLAN for their continued support.
We hope that these proceedings will serve as a valuable reference for Erlang and BEAM-based language researchers, implementors, and practitioners, and that you will find this year’s program appealing and thought-provoking.

Papers

Machine-Checked Natural Semantics for Core Erlang: Exceptions and Side Effects
Péter Bereczky, Dániel Horpácsi, and Simon J. Thompson
(Eötvös Loránd University, Hungary; University of Kent, UK)
This research is part of a wider project that aims to investigate and reason about the correctness of scheme-based source code transformations of Erlang programs. In order to formally reason about the definition of a programming language and the software built using it, we need a mathematically rigorous description of that language.
In this paper, we present an extended natural semantics for Core Erlang based on our previous formalisation implemented with the Coq Proof Assistant. This extension includes the concepts of exceptions and side effects, moreover, some modifications and updates are also discussed. Then we describe theorems about the properties of this formalisation (e.g. determinism), formal expression evaluation and equivalence examples. These equivalences can be interpreted as simple local refactorings.

Publisher's Version Article Search
Teaching Practical Realistic Verification of Distributed Algorithms in Erlang with TLA+
Peter Zeller, Annette Bieniusa, and Carla Ferreira
(TU Kaiserslautern, Germany; Nova University of Lisbon, Portugal)
Distributed systems are inherently complex as they need to address the interplay between features like communication, concurrency, and failure. Due to the inherent complexity of these interacting features, it is typically not possible to systematically test these kind of systems; yet, unexpected and unlikely combinations of events might cause corner cases that are hard to find. But since these systems are running typically for long durations, these events are likely to materialize eventually and must be handled correctly. Caught in such a dilemma, students are able to experience the benefits of applying verification tools to check their own algorithms and implementations. Having executable models with automatically generated executions allows them to experiment with different solutions by iteratively adapting and refining their algorithms.
In this experience report, we report on our experience of teaching verification in a (hands-on) distributed systems course. We argue that broadcast algorithms provide a sweet spot in design and verification complexity. To this end, we give an implementation of these algorithms in Erlang and derive a TLA+ specification. TLA+ is a formal language for describing and reasoning about distributed and concurrent systems and provides a model checker, TLC, among other things. Our study reveals interesting parallels between the Erlang and TLA+ code, while exposing the challenges of formally modeling communication and parallelism in distributed systems. Presenting selected aspects of our course design, we aim to motivate the feasibility and need for introducing verification in close correspondence to programming tasks.

Publisher's Version Article Search
Transformations towards Clean Functional Code
Boldizsár Poór, Melinda Toth, and István Bozó
(Eötvös Loránd University, Hungary)
The programming style has an impact on the readability and comprehensibility of the source code, and it may also affect run-time performance. This statement also holds for functional languages when the functional style is mixed with imperative design. In this paper, we present a couple of methods that can refactor imperatively styled Erlang source-code into a more functionally styled one. This can be done by transforming unnecessary calls to length, hd and tl into pattern matching or by lifting particular nested expressions. The results of our investigations indicate that these refactorings can not only shorten the length of the source code but also affect the complexity/readability. In this paper, we present some refactorings; moreover, real-life examples and data for its validation.

Publisher's Version Article Search
Secure Design and Verification of Erlang Systems
Viktória Fördős
(Cisco Systems, Sweden)
Security is a critical part of software development, companies have the utmost responsibility to protect their customers data against any threat. Secure design is a key enabler, since it cultivates security awareness in software projects from day zero. In this paper it is shown how to apply the principles of secure design to Erlang software projects. An Erlang specific method to identify trust zones is presented. The high risk vulnerabilities of the Erlang ecosystem are reviewed and grouped together using the CIA triad model. A dataflow based static analysis together with a prototype to verify security posture of a trust zone are introduced and evaluated using Riak Core as a case study.

Publisher's Version Article Search
Clojerl: The Expressive Power of Clojure on the BEAM
Juan Facorro and Natalia Chechina
(Bournemouth University, UK)
The development of new features and approaches in programming languages is a continuous and never-ending task, as languages are ultimately tools for expressing and solving problems. The past decade has seen a surge in languages implemented for the BEAM as part of a search to combine the fault-tolerance and scalability of the BEAM with a set of desired language features.
In this paper we present Clojerl, an implementation of the Clojure language with a rich set of data processing capabilities and the expressive power of Lisp for the BEAM. The main design principles of Clojerl are to provide (1) seamless interoperability with the BEAM to enable frictionless interaction with other BEAM languages and (2) portability with Clojure to enable existing Clojure code to run on the BEAM with little or no modifications. We evaluate Clojerl by running a set of experiments that analyse the performance of eight most widely used expressions. While the results of complex expressions show that Clojerl requires further optimisations, Clojerl significantly outperforms Clojure in a set of basic expressions, confirming that Clojerl has the potential to provide a competitive performance while offering a rich set of programming language features.

Publisher's Version Article Search

proc time: 0.28