Peter Van Roy

Professor at ICTEAM Institute, Université catholique de Louvain

Peter coordinated the recently finished LightKone Horizon 2020 project that has built Erlang-based platforms for general-purpose computing with Internet of Things. He is a contributor to the Mozart Programming System and is author of the textbook "Concepts, Techniques, and Models of Computer Programming", that has been translated into Polish (published by Helion).

A Family of λ-Calculi with Ports

Distributed systems programming exhibits a considerable degree of mostly-functional behaviour. On the other hand, programming every distributed system with no side-effect whatsoever is not realistic. Observational purity lends itself as a plausible alternative.
To exercise that choice for programming distributed systems, we present the λ(port) family of λ-Calculi. Ports and pure blocks are two characteristics of this family. Ports are the only single source of side-effects in the λ(port) family. Pure blocks are their linguistic support for declaring observational purity. Notably, pure blocks specify which nodes in the distributed system they are pure for. We promote a programming paradigm, in which, the programmer strives to maximise pure blocks and only leave the unavoidably effectful computations outside. Our paradigm brings added value to speculative execution, mock testing, distributed garbage collection, partial order reduction, and treatments of flaky tests.
We start the λ(port) family from its most basic member, in which messages are delivered instantly. We prove that observational equivalences of the more basic members of the family are retained upon addition of message delay, message loss, node failure, and network partitions. As such, one can freely prove observational equivalences in the most basic member without worrying about any of the successor features.

Video ←Back