Seyed Hossein Haeri

Programming Languages Scientist, Post-Doctoral Research Fellow

Hossein likes both the theory and practice of programming languages.

What he likes even more is reconciling the two. Hossein has an emerging interest in distributed systems programming. He worked in two very successful EU projects on the latter topic: SyncFree and LightKone.

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