Distributed Lazy Evaluation: A Big-Step Mechanised Semantics

This paper presents a big-step operational semantics for distributed lazy evaluation. Our semantics is an extension to the famous heap-based semantics of Launchbury for lazy evaluation. The high level of abstraction in our semantics helps us to easily prove different properties that are of interest to task distribution. Most importantly, we give criteria which establish a notion of bisimilarity between heaps. We also prove the validity of an induction principle that is used for proving observational equivalence between programs written in our system. Additionally, we briefly report the mechanisation of our semantics.