A formal semantics of the MULTI-ML language

In the context of high performance computing, it is important to avoid indeterminism and dead-locks. MULTI-ML is a functional parallel programming language "a la ML", designed to program hierarchical architectures in a structured way. It is based of the MULTI-BSP bridging model. To ensure that a program "cannot go wrong", we first need to define how a program "goes". To do so, we propose a formal operational semantics of the MULTI-ML language to ensure the properties of the MULTI-BSP model. We first describe a core-language and then introduce the big step's semantics evaluation rules. Then, we propose a set of evaluation rules that describe the behaviour of the MULTI-ML language. The memory model is also precisely defined, as the MULTI-BSP model deals with multiple level of nested memories.